aws · robin-aws · May 13, 2020 · May 14, 2020 · May 14, 2020 · May 21, 2020
diff --git a/buildspec.yml b/buildspec.yml
@@ -17,7 +17,7 @@ phases:
       # Although Dafny does have releases, we often need a newer hash than the latest release, while still needing the
       # the security of reproducible builds.
       - cd dafny
-      - git reset --hard df707bc07e3c39390286dfd0c1576d0a3f556f8b
+      - git reset --hard 4a98e283d5608cd7bd623be2b90f96a1d9eb557b
       - cd ..
       - nuget restore dafny/Source/Dafny.sln
       - msbuild dafny/Source/Dafny.sln

diff --git a/src/Crypto/RSAEncryption.dfy b/src/Crypto/RSAEncryption.dfy
@@ -17,8 +17,7 @@ module {:extern "RSAEncryption"} RSAEncryption {
   newtype {:nativeType "int", "number"} StrengthBits = x | 81 <= x < (0x8000_0000) witness 81
 
   // This trait represents the parent for RSA public and private keys
-  trait {:termination false} Key {
-    ghost var Repr: set<object>
+  trait {:termination false} Key extends Validatable {
     ghost const strength: StrengthBits
     ghost const padding: PaddingMode
     const pem: seq<uint8>

diff --git a/src/KMS/KMSUtils.dfy b/src/KMS/KMSUtils.dfy
@@ -120,12 +120,7 @@ module {:extern "KMSUtils"} KMSUtils {
 
   method {:extern "KMSUtils.ClientHelper", "AddCachingClientCallback"} AddCachingClientCallback(client: IAmazonKeyManagementService, region: Option<string>, cache: CachingClientSupplierCache)
 
-  trait {:extern "DafnyAWSKMSClientSupplier"} DafnyAWSKMSClientSupplier {
-    ghost var Repr: set<object>
-
-    predicate Valid()
-      reads this, Repr
-      ensures Valid() ==> this in Repr
+  trait {:extern "DafnyAWSKMSClientSupplier"} DafnyAWSKMSClientSupplier extends Validatable {
 
     method GetClient(region: Option<string>) returns (res: Result<IAmazonKeyManagementService>)
       requires Valid()
@@ -227,8 +222,7 @@ module {:extern "KMSUtils"} KMSUtils {
     }
   }
 
-  class CachingClientSupplierCache {
-    ghost var Repr: set<object>
+  class CachingClientSupplierCache extends Validatable {
     var ClientCache: map<Option<string>, IAmazonKeyManagementService>
 
     predicate Valid()
@@ -276,8 +270,8 @@ module {:extern "KMSUtils"} KMSUtils {
       ensures Valid() ==> this in Repr
     {
       this in Repr &&
-      clientSupplier in Repr && clientSupplier.Repr <= Repr && this !in clientSupplier.Repr && clientSupplier.Valid() &&
-      clientCache in Repr && clientCache.Repr <= Repr && this !in clientCache.Repr && clientCache.Valid() &&
+      ValidComponent(clientSupplier) &&
+      ValidComponent(clientCache) &&
       clientSupplier.Repr !! clientCache.Repr
     }
 

diff --git a/src/SDK/CMM/CachingCMM.dfy b/src/SDK/CMM/CachingCMM.dfy
@@ -67,8 +67,8 @@ module {:extern "CachingCMMDef"} CachingCMMDef {
       ensures Valid() ==> this in Repr
     {
       this in Repr &&
-      cmm in Repr && cmm.Repr <= Repr && this !in cmm.Repr && cmm.Valid() &&
-      cmc in Repr && cmc.Repr <= Repr && this !in cmc.Repr && cmc.Valid() &&
+      ValidComponent(cmm) &&
+      ValidComponent(cmc) &&
       cmm.Repr !! cmc.Repr
     }
 
@@ -144,7 +144,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef {
                                   returns (res: Result<Materials.ValidEncryptionMaterials>)
       requires Valid()
       modifies Repr
-      ensures Valid() && fresh(Repr - old(Repr))
+      ensures ValidAndFresh()
       ensures res.Success? ==> res.value.Serializable()
     {
       if materialsRequest.plaintextLength.None?
@@ -199,7 +199,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef {
                             returns (res: Result<Materials.ValidDecryptionMaterials>)
       requires Valid()
       modifies Repr
-      ensures Valid() && fresh(Repr - old(Repr))
+      ensures ValidAndFresh()
       ensures res.Success? ==> res.value.plaintextDataKey.Some?
     {
       var isSerializable := EncryptionContext.CheckSerializable(materialsRequest.encryptionContext);
@@ -295,8 +295,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef {
     res := Digest.Digest(CACHE_ID_HASH_ALGORITHM, wr.GetDataWritten());
   }
 
-  class CryptographicMaterialsCache {
-    ghost var Repr: set<object>
+  class CryptographicMaterialsCache extends Validatable {
     // The cache is split up into two independent maps, one for the encrypt path and one for the decrypt path.
     var EncryptMap: map<seq<uint8>, CacheEntryEncrypt>
     var DecryptMap: map<seq<uint8>, CacheEntryDecrypt>
@@ -338,7 +337,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef {
       requires Valid()
       requires encMat.Serializable()
       modifies Repr
-      ensures Valid() && fresh(Repr - old(Repr)) && entry in Repr
+      ensures ValidAndFresh() && entry in Repr
     {
       entry := new CacheEntryEncrypt(encMat, secondsToLiveLimit);
       Repr := Repr + {entry};
@@ -351,7 +350,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef {
       requires Valid()
       requires decMat.plaintextDataKey.Some?
       modifies Repr
-      ensures Valid() && fresh(Repr - old(Repr)) && entry in Repr
+      ensures ValidAndFresh() && entry in Repr
     {
       entry := new CacheEntryDecrypt(decMat, secondsToLiveLimit);
       Repr := Repr + {entry};
@@ -362,7 +361,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef {
     method EvictEncrypt(cacheID: seq<uint8>)
       requires Valid()
       modifies Repr
-      ensures Valid() && fresh(Repr - old(Repr))
+      ensures ValidAndFresh()
     {
       EncryptMap := map id | id in EncryptMap.Keys && id != cacheID :: EncryptMap[id];
     }
@@ -371,7 +370,7 @@ module {:extern "CachingCMMDef"} CachingCMMDef {
     method EvictDecrypt(cacheID: seq<uint8>)
       requires Valid()
       modifies Repr
-      ensures Valid() && fresh(Repr - old(Repr))
+      ensures ValidAndFresh()
     {
       DecryptMap := map id | id in DecryptMap.Keys && id != cacheID :: DecryptMap[id];
     }

diff --git a/src/SDK/CMM/DefaultCMM.dfy b/src/SDK/CMM/DefaultCMM.dfy
@@ -33,8 +33,7 @@ module {:extern "DefaultCMMDef"} DefaultCMMDef {
       reads this, Repr
       ensures Valid() ==> this in Repr
     {
-      this in Repr &&
-      keyring in Repr && keyring.Repr <= Repr && this !in keyring.Repr && keyring.Valid()
+      this in Repr && ValidComponent(keyring)
     }
 
     constructor OfKeyring(k: KeyringDefs.Keyring)

diff --git a/src/SDK/CMM/Defs.dfy b/src/SDK/CMM/Defs.dfy
@@ -15,17 +15,13 @@ module {:extern "CMMDefs"} CMMDefs {
   import Signature
   import EncryptionContext
 
-  trait {:termination false} CMM {
-    ghost var Repr: set<object>
-    predicate Valid()
-      reads this, Repr
-      ensures Valid() ==> this in Repr
+  trait {:termination false} CMM extends Validatable {
 
     method GetEncryptionMaterials(materialsRequest: Materials.EncryptionMaterialsRequest)
                                   returns (res: Result<Materials.ValidEncryptionMaterials>)
       requires Valid()
       modifies Repr
-      ensures Valid() && fresh(Repr - old(Repr))
+      ensures ValidAndFresh()
       ensures res.Success? ==> res.value.Serializable()
 
     // The following predicate is a synonym for Encryption.Serializable and provides a workaround for a translation bug
@@ -38,7 +34,7 @@ module {:extern "CMMDefs"} CMMDefs {
                             returns (res: Result<Materials.ValidDecryptionMaterials>)
       requires Valid()
       modifies Repr
-      ensures Valid() && fresh(Repr - old(Repr))
+      ensures ValidAndFresh()
       ensures res.Success? ==> res.value.plaintextDataKey.Some?
   }
 }
diff --git a/src/SDK/Keyring/Defs.dfy b/src/SDK/Keyring/Defs.dfy
@@ -12,11 +12,7 @@ module {:extern "KeyringDefs"} KeyringDefs {
   import Materials
   import AlgorithmSuite
 
-  trait {:termination false} Keyring {
-    ghost var Repr: set<object>
-    predicate Valid()
-      reads this, Repr
-      ensures Valid() ==> this in Repr
+  trait {:termination false} Keyring extends Validatable {
 
     method OnEncrypt(materials: Materials.ValidEncryptionMaterials) returns (res: Result<Materials.ValidEncryptionMaterials>)
       requires Valid()

diff --git a/src/SDK/Keyring/KMSKeyring.dfy b/src/SDK/Keyring/KMSKeyring.dfy
@@ -41,7 +41,7 @@ module {:extern "KMSKeyringDef"} KMSKeyringDef {
       && this in Repr
       && 0 <= |grantTokens| <= KMSUtils.MAX_GRANT_TOKENS
       && (|keyIDs| == 0 && generator.None? ==> isDiscovery)
-      && (clientSupplier in Repr && clientSupplier.Repr <= Repr && this !in clientSupplier.Repr && clientSupplier.Valid())
+      && ValidComponent(clientSupplier)
     }
 
     constructor (clientSupplier: KMSUtils.DafnyAWSKMSClientSupplier, keyIDs: seq<KMSUtils.CustomerMasterKey>, generator: Option<KMSUtils.CustomerMasterKey>, grantTokens: seq<KMSUtils.GrantToken>)

diff --git a/src/SDK/Keyring/MultiKeyring.dfy b/src/SDK/Keyring/MultiKeyring.dfy
@@ -42,8 +42,8 @@ module {:extern "MultiKeyringDef"} MultiKeyringDef {
           ensures Valid() ==> this in Repr
         {
             && this in Repr
-            && (generator != null ==> generator in Repr && generator.Repr <= Repr && generator.Valid())
-            && (forall j :: 0 <= j < |children| ==> children[j] in Repr && children[j].Repr <= Repr && children[j].Valid())
+            && (generator == null || ValidComponent(generator))
+            && (forall j :: 0 <= j < |children| ==> ValidComponent(children[j]))
         }
 
         method OnEncrypt(materials: Materials.ValidEncryptionMaterials) returns (res: Result<Materials.ValidEncryptionMaterials>)

diff --git a/src/SDK/Keyring/RawRSAKeyring.dfy b/src/SDK/Keyring/RawRSAKeyring.dfy
@@ -34,11 +34,9 @@ module {:extern "RawRSAKeyringDef"} RawRSAKeyringDef {
     {
       this in Repr &&
       (publicKey.Some? || privateKey.Some?) &&
-      (publicKey.Some? ==>
-        publicKey.get in Repr && publicKey.get.Repr <= Repr && this !in publicKey.get.Repr && publicKey.get.Valid()) &&
+      (publicKey.Some? ==> ValidComponent(publicKey.get)) &&
       (publicKey.Some? ==> publicKey.get.padding == paddingMode) &&
-      (privateKey.Some? ==>
-        privateKey.get in Repr && privateKey.get.Repr <= Repr && this !in privateKey.get.Repr && privateKey.get.Valid()) &&
+      (privateKey.Some? ==> ValidComponent(privateKey.get)) &&
       (privateKey.Some? ==> privateKey.get.padding == paddingMode) &&
       |keyNamespace| < UINT16_LIMIT &&
       |keyName| < UINT16_LIMIT

diff --git a/src/StandardLibrary/StandardLibrary.dfy b/src/StandardLibrary/StandardLibrary.dfy
@@ -6,6 +6,45 @@ include "UInt.dfy"
 module {:extern "STL"} StandardLibrary {
   import opened U = UInt
 
+  // A trait for objects with a Valid() predicate. Necessary in order to
+  // generalize some proofs, but also useful for reducing the boilerplate
+  // that most such objects need to include.
+  trait {:termination false} Validatable {
+    // TODO-RS: The style guide actually implies this should be "repr",
+    // but the convention is well-established at this point.
+    ghost var Repr: set<object>
+
+    predicate Valid()
+      reads this, Repr
+      ensures Valid() ==> this in Repr
+
+    // Convenience predicate for when your object's validity depends on one
+    // or more other objects.
+    predicate ValidComponent(component: Validatable)
+      reads this, Repr 
+      ensures ValidComponent(component) ==> (
+        && component in Repr
+        && component.Repr <= Repr
+        && this !in component.Repr
+        && component.Valid())
+    {
+      && component in Repr
+      && component.Repr <= Repr
+      && this !in component.Repr
+      && component.Valid()
+    }
+
+    // Convenience predicate, since you often want to assert that 
+    // new objects in Repr are fresh as well.
+    // TODO-RS: Better name?
+    twostate predicate ValidAndFresh() 
+      reads this, Repr
+      ensures ValidAndFresh() ==> Valid() && fresh(Repr - old(Repr))
+    {
+      Valid() && fresh(Repr - old(Repr))
+    }
+  }
+
   // TODO: Depend on types defined in dafny-lang/libraries instead
   datatype Option<+T> = None | Some(get: T)
   {

diff --git a/src/Util/Streams.dfy b/src/Util/Streams.dfy
@@ -7,8 +7,7 @@ module Streams {
   import opened StandardLibrary
   import opened UInt = StandardLibrary.UInt
 
-  class SeqReader<T> {
-    ghost var Repr: set<object>
+  class SeqReader<T> extends Validatable {
     const data: seq<T>
     var pos: nat
 
@@ -66,16 +65,14 @@ module Streams {
     }
   }
 
-  class ByteReader {
-    ghost var Repr: set<object>
+  class ByteReader extends Validatable {
     const reader: SeqReader<uint8>
 
     predicate Valid()
       reads this, Repr
       ensures Valid() ==> this in Repr
     {
-      this in Repr &&
-      reader in Repr && reader.Repr <= Repr && this !in reader.Repr && reader.Valid()
+      this in Repr && ValidComponent(reader)
     }
 
     constructor (s: seq<uint8>)
@@ -188,8 +185,7 @@ module Streams {
     }
   }
 
-  class SeqWriter<T> {
-    ghost var Repr: set<object>
+  class SeqWriter<T> extends Validatable {
     var data: seq<T>
 
     predicate Valid()
@@ -221,16 +217,14 @@ module Streams {
     }
   }
 
-  class ByteWriter {
-    ghost var Repr: set<object>
+  class ByteWriter extends Validatable {
     const writer: SeqWriter<uint8>
 
     predicate Valid()
       reads this, Repr
       ensures Valid() ==> this in Repr
     {
-      this in Repr &&
-      writer in Repr && writer.Repr <= Repr && this !in writer.Repr && writer.Valid()
+      this in Repr && ValidComponent(writer)
     }
 
     constructor()

diff --git a/test/SDK/CMM/CachingCMM.dfy b/test/SDK/CMM/CachingCMM.dfy
@@ -243,7 +243,7 @@ module TestCachingCMM {
                                     returns (res: Result<Materials.ValidEncryptionMaterials>)
         requires Valid()
         modifies Repr
-        ensures Valid() && fresh(Repr - old(Repr))
+        ensures ValidAndFresh()
         ensures res.Success? ==> res.value.plaintextDataKey.Some? && res.value.Serializable()
       {
         TestUtils.ExpectSerializableEncryptionContext(materialsRequest.encryptionContext);
@@ -279,7 +279,7 @@ module TestCachingCMM {
                               returns (res: Result<Materials.ValidDecryptionMaterials>)
         requires Valid()
         modifies Repr
-        ensures Valid() && fresh(Repr - old(Repr))
+        ensures ValidAndFresh()
         ensures res.Success? ==> res.value.plaintextDataKey.Some?
       {
         var dm := Materials.DecryptionMaterials(