chore: Use latest Dafny version (#302)

* chore: Use latest Dafny version

* chore: Update Boogie version to 2.4.21.

Note, Boogie versions 2.5 and later want Z3 4.8.7, which Dafny doesn't yet support.

* chore: Update/speed up some proofs.

Author: RustanLeino

buildspec.yml

@@ -10,15 +10,15 @@ phases:
       - mozroots --import --sync
       # Get Boogie
       # Multiple Boogie commits have broken our build or test cases. Locking down Boogie.
-      - git clone --branch v2.4.2 https://github.com/boogie-org/boogie.git
+      - git clone --branch v2.4.21 https://github.com/boogie-org/boogie.git
       - nuget restore boogie/Source/Boogie.sln
       - msbuild boogie/Source/Boogie.sln
       # Get Dafny
       - git clone https://github.com/microsoft/dafny.git
       # 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 5ca6ef8347c9675b6824e987967925b1208ca47c
+      - git reset --hard df707bc07e3c39390286dfd0c1576d0a3f556f8b
       - cd ..
       - nuget restore dafny/Source/Dafny.sln
       - msbuild dafny/Source/Dafny.sln

src/KMS/KMSUtils.dfy

@@ -13,7 +13,8 @@ module {:extern "KMSUtils"} KMSUtils {
 
   const MAX_GRANT_TOKENS := 10
 
-  type CustomerMasterKey = s: string | ValidFormatCMK(s) witness "alias/ExampleAlias"
+  type CustomerMasterKey = s: string | ValidFormatCMK(s)
+    witness (ValidCMKAliasFromSuffix("ExampleAlias"); "alias/ExampleAlias")
 
   predicate method ValidFormatCMK(cmk: string) {
     ValidFormatCMKKeyARN(cmk) || ValidFormatCMKAlias(cmk) || ValidFormatCMKAliasARN(cmk)
@@ -29,6 +30,32 @@ module {:extern "KMSUtils"} KMSUtils {
     UTF8.IsASCIIString(cmk) && 0 < |cmk| <= 2048 && |components| == 2 && components[0] == "alias"
   }
 
+  lemma ValidCMKAliasFromSuffix(suffix: string)
+    requires UTF8.IsASCIIString(suffix) && |suffix| < 2042 && '/' !in suffix
+    ensures var cmk := "alias/" + suffix;
+      ValidFormatCMKAlias(cmk)
+  {
+    var alias := "alias";
+    assert UTF8.IsASCIIString(alias);
+    var cmk := alias + "/" + suffix;
+    assert UTF8.IsASCIIString(cmk);
+
+    var components := Split(cmk, '/');
+    calc {
+      components;
+    ==
+      Split(alias + "/" + suffix, '/');
+    ==  { WillSplitOnDelim(cmk, '/', alias); }
+      [alias] + Split(cmk[|alias| + 1..], '/');
+    ==  { assert cmk[|alias| + 1..] == suffix; }
+      [alias] + Split(suffix, '/');
+    ==  { WillNotSplitWithOutDelim(suffix, '/'); }
+      [alias] + [suffix];
+    ==
+      [alias, suffix];
+    }
+  }
+
   predicate method ValidFormatCMKAliasARN(cmk: string) {
     var components := Split(cmk, ':');
     UTF8.IsASCIIString(cmk) && 0 < |cmk| <= 2048 && |components| == 6 && components[0] == "arn" && components[2] == "kms" && Split(components[5], '/')[0] == "alias"