From 55399db1d51f882f0be36ac75d798fa5d7bafd43 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 22 Aug 2024 14:16:56 -0700 Subject: [PATCH] fix: Remove uses of `:|` (#618) 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. --- .../src/CMMs/DefaultCMM.dfy | 22 ++++++++++++++----- .../src/CMMs/RequiredEncryptionContextCMM.dfy | 16 +++++--------- .../src/CanonicalEncryptionContext.dfy | 3 ++- AwsCryptographyPrimitives/test/TestRSA.dfy | 15 +++++++------ libraries | 2 +- 5 files changed, 33 insertions(+), 25 deletions(-) diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy index 7b40aa215..0237bce12 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy @@ -23,6 +23,7 @@ module DefaultCMM { import Defaults import Commitment import Seq + import SortedSets class DefaultCMM extends CMM.VerifiableInterface @@ -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) @@ -478,17 +479,24 @@ 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.encryptionContext - && key !in keysSet + && key !in keysSet' :: input.reproducedEncryptionContext.value[key] == input.encryptionContext[key] 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( @@ -496,7 +504,11 @@ module DefaultCMM { } 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(); + } } } diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy index 88df3881f..3c7ef0366 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy @@ -16,6 +16,7 @@ module RequiredEncryptionContextCMM { import UTF8 import Types = AwsCryptographyMaterialProvidersTypes import Seq + import SortedSets class RequiredEncryptionContextCMM extends CMM.VerifiableInterface @@ -52,17 +53,10 @@ 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); + assert |keySeq| == |keySet| == |inputKeys|; + assert forall k <- keySeq + :: k in inputKeys; underlyingCMM := inputCMM; requiredEncryptionContextKeys := keySeq; diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CanonicalEncryptionContext.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CanonicalEncryptionContext.dfy index ad1ef54fa..91b3ac34a 100644 --- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CanonicalEncryptionContext.dfy +++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CanonicalEncryptionContext.dfy @@ -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'] @@ -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); if |keys| == 0 then Success([]) diff --git a/AwsCryptographyPrimitives/test/TestRSA.dfy b/AwsCryptographyPrimitives/test/TestRSA.dfy index 2aafde804..2b9f25d8c 100644 --- a/AwsCryptographyPrimitives/test/TestRSA.dfy +++ b/AwsCryptographyPrimitives/test/TestRSA.dfy @@ -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" @@ -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, @@ -144,7 +146,6 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { KeyFromGenerateRSAKeyPair ); - allPadding := allPadding - {padding}; } } @@ -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( @@ -178,7 +180,6 @@ module {:options "-functionSyntax:4"} TestAwsCryptographyPrimitivesRSA { KeyFromTestVectorsPair ); - allPadding := allPadding - {padding}; } } diff --git a/libraries b/libraries index e9b898d0e..dbb1949da 160000 --- a/libraries +++ b/libraries @@ -1 +1 @@ -Subproject commit e9b898d0ec08e129b8e61306b2617b36c4ce5d3e +Subproject commit dbb1949da0e610bd0cc0dfe1ecc751808e928dc4