chore: Improve compatibility with Dafny 4.4 (#129)

* Some small changes to verify with Dafny 4.4 * Improve proof of ValidUTF8Concat * Undo OnDecrypt' change for now * Undo submodule bump * Add two more small changes for Dafny 4.4 --------- Co-authored-by: Aaron Tomb <[email protected]> Co-authored-by: Aaron Tomb <[email protected]>
aws · Nov 30, 2023 · a6edf30 · a6edf30
1 parent 3d10796
commit a6edf30
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 17 deletions.
diff --git a/...ptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy b/...ptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy
@@ -260,7 +260,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
     if s[0] == v then 0 else 1 + IndexOfCacheEntry(s[1..], v)
   }
 
-  method RemoveValue<K, V>(k0: K, m: map<K, V>)
+  method RemoveValue<K, V(==)>(k0: K, m: map<K, V>)
     requires k0 in m
     requires forall k <- m, k' <- m | k != k' :: m[k] != m[k']
     ensures (m - {k0}).Values == m.Values - {m[k0]}

diff --git a/...alProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/...alProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy
@@ -848,7 +848,7 @@ module AwsKmsKeyring {
       && client.Modifies == Modifies
     }
 
-    predicate Ensures(
+    predicate {:vcs_split_on_every_assert} Ensures(
       input: MaterialWrapping.GenerateAndWrapInput,
       res: Result<MaterialWrapping.GenerateAndWrapOutput<KmsWrapInfo>, Types.Error>,
       attemptsState: seq<ActionInvoke<MaterialWrapping.GenerateAndWrapInput, Result<MaterialWrapping.GenerateAndWrapOutput<KmsWrapInfo>, Types.Error>>>

diff --git a/StandardLibrary/src/Base64.dfy b/StandardLibrary/src/Base64.dfy
@@ -363,7 +363,7 @@ module Base64 {
       DecodeUnpadded(s)
   }
 
-  lemma AboutDecodeValid(s: seq<char>, b: seq<uint8>)
+  lemma {:vcs_split_on_every_assert} AboutDecodeValid(s: seq<char>, b: seq<uint8>)
     requires IsBase64String(s) && b == DecodeValid(s)
     ensures 4 <= |s| ==> var finalBlockStart := |s| - 4;
                          var prefix, suffix := s[..finalBlockStart], s[finalBlockStart..];

diff --git a/StandardLibrary/src/UTF8.dfy b/StandardLibrary/src/UTF8.dfy
@@ -181,20 +181,9 @@ module {:extern "UTF8"} UTF8 {
         lo := lo + 4;
       }
     }
-    calc {
-      ValidUTF8Seq(s + t);
-    ==  // def.ValidUTF8Seq
-      ValidUTF8Range(s + t, 0, |s + t|);
-    ==  // loop invariant
-      ValidUTF8Range(s + t, lo, |s + t|);
-    ==  { assert s + t == s + t + [] && lo == |s| && |s + t| == |s| + |t|; }
-      ValidUTF8Range(s + t + [], |s|, |s| + |t|);
-    ==  { ValidUTF8Embed(s, t, [], 0, |t|); }
-      ValidUTF8Range(t, 0, |t|);
-    ==  // def.ValidUTF8Seq
-      ValidUTF8Seq(t);
-    ==  // precondition
-      true;
+    assert ValidUTF8Seq(s + t) by {
+      ValidUTF8Embed(s, t, [], 0, |t|);
+      assert s + t == s + t + [] && lo == |s|;
     }
   }
 }