Skip to content

Commit

Permalink
fix: Remove uses of :| (#618)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
atomb authored and texastony committed Aug 23, 2024
1 parent 01656da commit 0ca4c38
Show file tree
Hide file tree
Showing 5 changed files with 33 additions and 25 deletions.
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 @@ -478,25 +479,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.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(
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
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,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;

Expand Down
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);

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

0 comments on commit 0ca4c38

Please sign in to comment.