feat: Upgrade to Dafny 4.0 (#151)

Co-authored-by: Valerie Lambert <lavaleri@amazon.com> Co-authored-by: Alex Chew <alex-chew@users.noreply.github.com>
smithy-lang · Apr 13, 2023 · 014ff37 · 014ff37
1 parent 39eaa78
commit 014ff37
Show file tree

Hide file tree

Showing 30 changed files with 217 additions and 108 deletions.
diff --git a/AwsCryptographicMaterialProviders/Makefile b/AwsCryptographicMaterialProviders/Makefile
@@ -12,7 +12,7 @@ PROJECT_SERVICES := \
 SERVICE_NAMESPACE_AwsCryptographicMaterialProviders=aws.cryptography.materialProviders
 SERVICE_NAMESPACE_AwsCryptographyKeyStore=aws.cryptography.keyStore
 
-MAX_RESOURCE_COUNT=50000000
+MAX_RESOURCE_COUNT=60000000
 # Order is important
 # In java they MUST be built
 # in the order they depend on each other

diff --git a/...ptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsArnParsing.dfy b/...ptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsArnParsing.dfy
@@ -230,6 +230,13 @@ module AwsArnParsing {
  {}
 
  function method ParseAwsKmsArn(identifier: string): (result: Result<AwsKmsArn, string>)
+ ensures result.Success? ==>
+ && "arn" <= identifier
+ && |Split(identifier, ':')| == 6
+ && |Split(identifier, ':')[1]| > 0
+ && Split(identifier, ':')[2] == "kms"
+ && |Split(identifier, ':')[3]| > 0
+ && |Split(identifier, ':')[4]| > 0
  {
  var components := Split(identifier, ':');
 
@@ -252,6 +259,13 @@ module AwsArnParsing {
  }
 
  function method ParseAmazonDynamodbTableArn(identifier: string): (result: Result<AmazonDynamodbTableArn, string>)
+ ensures result.Success? ==>
+ && "arn" <= identifier
+ && |Split(identifier, ':')| == 6
+ && |Split(identifier, ':')[1]| > 0
+ && Split(identifier, ':')[2] == "dynamodb"
+ && |Split(identifier, ':')[3]| > 0
+ && |Split(identifier, ':')[4]| > 0
  {
  var components := Split(identifier, ':');
 

diff --git a/...ptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy b/...ptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy
@@ -182,7 +182,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
  assert (head.Ptr? <==> tail.Ptr?);
  }
 
- method remove(toRemove: CacheEntry)
+ method {:vcs_split_on_every_assert} remove(toRemove: CacheEntry)
  requires Invariant()
  requires toRemove in Items
  modifies this, Items
@@ -280,6 +280,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
 
  ghost predicate ValidState()
  reads this`Modifies, Modifies - {History}
+ ensures ValidState() ==> History in Modifies
  {
  && History in Modifies
  && this in Modifies
@@ -297,7 +298,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
  // The cache is a cache of Cells, these Cells MUST be unique.
  // The actual value that the Cell contains MAY be a duplicate.
  // See the uniqueness comment on the DoublyLinkedList.Invariant.
- && (forall k <- cache.Keys(), k' <- cache.Keys() | k != k' :: cache.Select(k) != cache.Select(k'))
+ && MutableMapIsInjective(cache)
  // Given that cache.Values and queue.Items are unique
  // they MUST contain exactly the same elements.
  && multiset(cache.Values()) == multiset(queue.Items)
@@ -410,7 +411,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
  ghost predicate PutCacheEntryEnsuresPublicly(input: Types.PutCacheEntryInput, output: Result<(), Types.Error>)
  {true}
 
- method PutCacheEntry'(input: Types.PutCacheEntryInput)
+ method {:vcs_split_on_every_assert} PutCacheEntry'(input: Types.PutCacheEntryInput)
  returns (output: Result<(), Types.Error>)
  requires ValidState()
  modifies Modifies - {History}
@@ -484,7 +485,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
  ghost predicate DeleteCacheEntryEnsuresPublicly(input: Types.DeleteCacheEntryInput, output: Result<(), Types.Error>)
  {true}
 
- method DeleteCacheEntry'(input: Types.DeleteCacheEntryInput)
+ method {:vcs_split_on_every_assert} DeleteCacheEntry'(input: Types.DeleteCacheEntryInput)
  returns (output: Result<(), Types.Error>)
  requires ValidState()
  modifies Modifies - {History}
@@ -510,11 +511,29 @@ module {:options "/functionSyntax:4" } LocalCMC {
  // to keep others from using this value.
  // This is "more" thread safe.
  cache.Remove(input.identifier);
- assert |cache.Keys()| <= |old@CAN_REMOVE(cache.Keys())|;
+ assert cell !in cache.Values();
+
+ assert MutableMapIsInjective(cache) by {
+ // Since the map values are themselves heap objects, we need to check that they too are unchanged
+ assert forall k <- cache.Keys() :: old(allocated(cache.Select(k))) && unchanged(cache.Select(k));
+ assert MutableMapIsInjective(old@CAN_REMOVE(cache));
+
+ assert MutableMapContains(old@CAN_REMOVE(cache), cache);
+ LemmaMutableMapContainsPreservesInjectivity(old@CAN_REMOVE(cache), cache);
+ }
+ assert |cache.Keys()| == |old@CAN_REMOVE(cache.Keys())| - 1;
  assert cache.Size() <= old@CAN_REMOVE(cache.Size()) <= entryCapacity;
  queue.remove(cell);
+ assert multiset(cache.Values()) == multiset(queue.Items) by {
+ var cacheMultiset := multiset(cache.Values());
+ var queueMultiset := multiset(queue.Items);
+ assert cacheMultiset[cell := 0] == queueMultiset[cell := 0];
+ assert cell !in cacheMultiset;
+ assert cell !in queueMultiset;
+ }
  Modifies := Modifies - {cell};
  }
+
  output := Success(());
  }
 
@@ -602,4 +621,26 @@ module {:options "/functionSyntax:4" } LocalCMC {
  return Success(());
  }
  }
+
+ // TODO move this into MutableMap
+ ghost predicate MutableMapIsInjective<K, V>(m: MutableMap<K, V>)
+ reads m
+ {
+ forall k <- m.Keys(), k' <- m.Keys() | k != k' :: m.Select(k) != m.Select(k')
+ }
+
+ // TODO move this into MutableMap
+ ghost predicate MutableMapContains<K, V>(big: MutableMap<K, V>, small: MutableMap<K, V>)
+ reads {big, small}
+ {
+ && small.Keys() <= big.Keys()
+ && forall k <- small.Keys() :: small.Select(k) == big.Select(k)
+ }
+
+ // TODO move this into MutableMap
+ lemma LemmaMutableMapContainsPreservesInjectivity<K, V>(big: MutableMap<K, V>, small: MutableMap<K, V>)
+ requires MutableMapContains(big, small)
+ requires MutableMapIsInjective(big)
+ ensures MutableMapIsInjective(small)
+ {}
 }
diff --git a/...dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/...dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy
@@ -603,7 +603,7 @@ module AwsKmsHierarchicalKeyring {
  }
  }
 
- method SortByTime(queryResponse: DDB.ItemList)
+ method {:vcs_split_on_every_assert} SortByTime(queryResponse: DDB.ItemList)
  returns (output: branchKeyItem)
  requires |queryResponse| > 0
  requires 

diff --git a/...afny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy b/...afny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy
@@ -20,7 +20,7 @@ module MrkAwareStrictMultiKeyring {
  import AwsKmsMrkKeyring
  import opened AwsKmsUtils
 
- method MrkAwareStrictMultiKeyring(
+ method {:vcs_split_on_every_assert} MrkAwareStrictMultiKeyring(
  generator: Option<string>,
  awsKmsKeys: Option<seq<string>>,
  clientSupplier: Types.IClientSupplier,

diff --git a/...viders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy b/...viders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy
@@ -20,7 +20,7 @@ module StrictMultiKeyring {
  import AwsKmsKeyring
  import opened AwsKmsUtils
 
- method StrictMultiKeyring(
+ method {:vcs_split_on_every_assert} StrictMultiKeyring(
  generator: Option<string>,
  awsKmsKeys: Option<seq<string>>,
  clientSupplier: Types.IClientSupplier,

diff --git a/...icMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy b/...icMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy
@@ -186,6 +186,7 @@ module MultiKeyring {
  for i := 0 to |this.childKeyrings|
  invariant returnMaterials.plaintextDataKey.Some?
  invariant unchanged(History);
+ invariant i < |this.childKeyrings| ==> this.childKeyrings[i].Modifies <= Modifies
  {
  var onEncryptInput := Types.OnEncryptInput(materials := returnMaterials);
 

diff --git a/AwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts b/AwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts
@@ -52,7 +52,7 @@ repositories {
 }
 
 dependencies {
- implementation("dafny.lang:DafnyRuntime:3.10.0")
+ implementation("org.dafny:DafnyRuntime:4.0.0")
  implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
  implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
  implementation("software.amazon.cryptography:AwsCryptographyPrimitives:1.0-SNAPSHOT")

diff --git a/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj b/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj
@@ -11,7 +11,7 @@
 
  <ItemGroup>
  <PackageReference Include="AWSSDK.Core" Version="3.7.103" />
- <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+ <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
  <PackageReference Include="Portable.BouncyCastle" Version="1.8.5.2" />
  <!--
  System.Collections.Immutable can be removed once dafny.msbuild is updated with

diff --git a/AwsCryptographyPrimitives/Makefile b/AwsCryptographyPrimitives/Makefile
@@ -3,11 +3,10 @@
 
 CORES=2
 
-include ../SharedMakefile.mk
+include ../SharedMakefileV2.mk
 
 SMITHY_NAMESPACE=aws.cryptography.primitives
 MAX_RESOURCE_COUNT=10000000
-# Order is important
-# In java they MUST be built
-# in the order they depend on each other
-LIBRARIES := 
+
+STD_LIBRARY=StandardLibrary
+SMITHY_DEPS=model
diff --git a/AwsCryptographyPrimitives/runtimes/java/build.gradle.kts b/AwsCryptographyPrimitives/runtimes/java/build.gradle.kts
@@ -52,7 +52,7 @@ repositories {
 }
 
 dependencies {
- implementation("dafny.lang:DafnyRuntime:3.10.0")
+ implementation("org.dafny:DafnyRuntime:4.0.0")
  implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
  implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
  implementation("org.bouncycastle:bcprov-jdk18on:1.72")

diff --git a/AwsCryptographyPrimitives/runtimes/net/Crypto.csproj b/AwsCryptographyPrimitives/runtimes/net/Crypto.csproj
@@ -11,7 +11,7 @@
 
  <ItemGroup>
  <PackageReference Include="AWSSDK.Core" Version="3.7.12.2" />
- <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+ <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
  <PackageReference Include="Portable.BouncyCastle" Version="1.8.5.2" />
  <!--
  System.Collections.Immutable can be removed once dafny.msbuild is updated with

diff --git a/ComAmazonawsDynamodb/Makefile b/ComAmazonawsDynamodb/Makefile
@@ -3,12 +3,10 @@
 
 CORES=2
 
-include ../SharedMakefile.mk
+include ../SharedMakefileV2.mk
 
 SMITHY_NAMESPACE=com.amazonaws.dynamodb
 MAX_RESOURCE_COUNT=10000000
-# Order is important
-# In java they MUST be built
-# in the order they depend on each other
-LIBRARIES := 
-AWS_SDK_CMD := --aws-sdk
+AWS_SDK_CMD := --aws-sdk
+STD_LIBRARY=StandardLibrary
+SMITHY_DEPS=model
diff --git a/ComAmazonawsDynamodb/runtimes/java/build.gradle.kts b/ComAmazonawsDynamodb/runtimes/java/build.gradle.kts
@@ -52,7 +52,7 @@ repositories {
 }
 
 dependencies {
- implementation("dafny.lang:DafnyRuntime:3.10.0")
+ implementation("org.dafny:DafnyRuntime:4.0.0")
  implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
  implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
  implementation(platform("software.amazon.awssdk:bom:2.19.1"))

diff --git a/ComAmazonawsDynamodb/runtimes/net/ComAmazonawsDynamodb.csproj b/ComAmazonawsDynamodb/runtimes/net/ComAmazonawsDynamodb.csproj
@@ -10,7 +10,7 @@
  </PropertyGroup>
 
  <ItemGroup>
- <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+ <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
  <PackageReference Include="AWSSDK.Core" Version="3.7.103" />
  <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.101.8" />
  <!--

diff --git a/ComAmazonawsKms/Makefile b/ComAmazonawsKms/Makefile
@@ -3,12 +3,10 @@
 
 CORES=2
 
-include ../SharedMakefile.mk
+include ../SharedMakefileV2.mk
 
 SMITHY_NAMESPACE=com.amazonaws.kms
 MAX_RESOURCE_COUNT=10000000
-# Order is important
-# In java they MUST be built
-# in the order they depend on each other
-LIBRARIES := 
-AWS_SDK_CMD := --aws-sdk
+AWS_SDK_CMD := --aws-sdk
+STD_LIBRARY=StandardLibrary
+SMITHY_DEPS=model
diff --git a/ComAmazonawsKms/runtimes/java/build.gradle.kts b/ComAmazonawsKms/runtimes/java/build.gradle.kts
@@ -52,7 +52,7 @@ repositories {
 }
 
 dependencies {
- implementation("dafny.lang:DafnyRuntime:3.10.0")
+ implementation("org.dafny:DafnyRuntime:4.0.0")
  implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
  implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
  implementation(platform("software.amazon.awssdk:bom:2.19.1"))

diff --git a/ComAmazonawsKms/runtimes/net/AWS-KMS.csproj b/ComAmazonawsKms/runtimes/net/AWS-KMS.csproj
@@ -10,7 +10,7 @@
  </PropertyGroup>
 
  <ItemGroup>
- <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+ <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
  <PackageReference Include="AWSSDK.Core" Version="3.7.11.12" />
  <PackageReference Include="AWSSDK.KeyManagementService" Version="3.7.3.20" />
  <!--

diff --git a/Makefile b/Makefile
@@ -1,9 +1,20 @@
 
 
 verify:
- CORES=4 $(MAKE) -C AwsCryptographyPrimitives verify
- CORES=4 $(MAKE) -C ComAmazonawsKms verify
- CORES=4 $(MAKE) -C AwsCryptographicMaterialProviders verify
+ $(MAKE) -C StandardLibrary verify CORES=4
+ $(MAKE) -C AwsCryptographyPrimitives verify CORES=4
+ $(MAKE) -C ComAmazonawsKms verify CORES=4
+ $(MAKE) -C ComAmazonawsDynamodb verify CORES=4
+ $(MAKE) -C AwsCryptographicMaterialProviders verify CORES=4
+ $(MAKE) -C AwsEncryptionSDK verify CORES=4
+
+dafny-reportgenerator:
+ $(MAKE) -C StandardLibrary dafny-reportgenerator
+ $(MAKE) -C AwsCryptographyPrimitives dafny-reportgenerator
+ $(MAKE) -C ComAmazonawsKms dafny-reportgenerator
+ $(MAKE) -C ComAmazonawsDynamodb dafny-reportgenerator
+ $(MAKE) -C AwsCryptographicMaterialProviders dafny-reportgenerator
+ $(MAKE) -C AwsEncryptionSDK dafny-reportgenerator
 
 duvet: | duvet_extract duvet_report