Replace Require* methods with expect statements (#213)

Converting Require* calls to expects

Remove remaining Result<()> return values

Update Dafny commit reference

buildspec.yml

@@ -18,7 +18,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 3f31d66499ab5e2e5d9a7b21f541de5b1d3eb585
+      - git reset --hard 4ecab36652adc9ad67294e2232f1b763453c0de0
       - cd ..
       - nuget restore dafny/Source/Dafny.sln
       - msbuild dafny/Source/Dafny.sln

src/StandardLibrary/StandardLibrary.dfy

@@ -45,32 +45,6 @@ module {:extern "STL"} StandardLibrary {
     }
   }
 
-  function method RequireEqual<T(==)>(expected: T, actual: T): (r: Result<()>)
-      ensures r.Success? ==> expected == actual
-  {
-    // TODO: Report message similar to "Expected ___ but got ___"
-    // Blocked on https://github.com/dafny-lang/dafny/issues/450
-    RequireWithMessage(expected == actual, "Failed equality")
-  }
-
-  function method Require(b: bool): (r: Result<()>)
-      ensures r.Success? ==> b
-  {
-    RequireWithMessage(b, "Failed requirement")
-  }
-
-  function method RequireFailure<T>(x: Result<T>): (r: Result<()>)
-      ensures r.Success? ==> x.Failure?
-  {
-    RequireWithMessage(x.Failure?, "Expected failure, but got success")
-  }
-
-  function method RequireWithMessage(b: bool, message: string): (r: Result<()>)
-      ensures r.Success? ==> b
-  {
-    if b then Success(()) else Failure(message)
-  }
-
   function method Join<T>(ss: seq<seq<T>>, joiner: seq<T>): (s: seq<T>)
     requires 0 < |ss|
   {

test/Crypto/Signature.dfy

@@ -9,44 +9,43 @@ module TestSignature {
   import Signature
   import UTF8
 
-  method YCompression(s: Signature.ECDSAParams, fieldSize: nat) returns (r: Result<()>) {
-    var res :- Signature.KeyGen(s);
+  method YCompression(s: Signature.ECDSAParams, fieldSize: nat) {
+    var res :- expect Signature.KeyGen(s);
     var public, secret := res.verificationKey, res.signingKey;
     // This is the declared postcondition of the natively implemented KenGen method, plus a condition
     // about zero-padding:
-    var _ :- Require(0 < |secret|);
-    var _ :- Require(|public| == 1 + (fieldSize + 7) / 8);  // 1 byte for y; x zero-padded up to the field size
-    var _ :- Require(public[0] == 2 || public[0] == 3);  // public key uses y compression
-    return Success(());
+    expect 0 < |secret|;
+    expect |public| == 1 + (fieldSize + 7) / 8;  // 1 byte for y; x zero-padded up to the field size
+    expect public[0] == 2 || public[0] == 3;  // public key uses y compression
   }
 
-  method {:test} YCompression384() returns (r: Result<()>) {
-    r := YCompression(Signature.ECDSA_P384, 384);
+  method {:test} YCompression384() {
+    YCompression(Signature.ECDSA_P384, 384);
   }
 
-  method {:test} YCompression256() returns (r: Result<()>) {
-    r := YCompression(Signature.ECDSA_P256, 256);
+  method {:test} YCompression256() {
+    YCompression(Signature.ECDSA_P256, 256);
   }
 
-  method VerifyMessage(params: Signature.ECDSAParams) returns (r: Result<()>){
-    var message :- UTF8.Encode("Hello, World!");
-    var keys :- Signature.KeyGen(params);
-
-    var digest :- Signature.Digest(params, message);
-    var signature :- Signature.Sign(params, keys.signingKey, digest);
-    var shouldBeTrue :- Signature.Verify(params, keys.verificationKey, digest, signature);
-    var _ :- Require(shouldBeTrue);
-    var badDigest :- Signature.Digest(params, message + [1]);
-    var shouldBeFalse :- Signature.Verify(params, keys.verificationKey, badDigest, signature);
-    var _ :- Require(!shouldBeFalse);
-    return Success(());
+  method VerifyMessage(params: Signature.ECDSAParams) {
+    var message :- expect UTF8.Encode("Hello, World!");
+    var keys :- expect Signature.KeyGen(params);
+
+    var digest :- expect Signature.Digest(params, message);
+    var signature :- expect Signature.Sign(params, keys.signingKey, digest);
+    var shouldBeTrue :- expect Signature.Verify(params, keys.verificationKey, digest, signature);
+    expect shouldBeTrue;
+
+    var badDigest :- expect Signature.Digest(params, message + [1]);
+    var shouldBeFalse :- expect Signature.Verify(params, keys.verificationKey, badDigest, signature);
+    expect !shouldBeFalse;
   }
 
-  method {:test} VerifyMessage384() returns (r: Result<()>) {
-    r := VerifyMessage(Signature.ECDSA_P384);
+  method {:test} VerifyMessage384() {
+    VerifyMessage(Signature.ECDSA_P384);
   }
 
-  method {:test} VerifyMessage256() returns (r: Result<()>) {
-    r := VerifyMessage(Signature.ECDSA_P256);
+  method {:test} VerifyMessage256() {
+    VerifyMessage(Signature.ECDSA_P256);
   }
 }

test/KMS/Integration.dfy

@@ -25,16 +25,16 @@ module IntegTestKMS {
   import UTF8
   import Base64
 
-  method EncryptDecryptTest(cmm: CMMDefs.CMM, message: string) returns (res: Result<string>)
+  method EncryptDecryptTest(cmm: CMMDefs.CMM, message: string) returns (res: string)
     requires cmm.Valid()
   {
     var encodedMsg: seq<uint8>;
     var encodeResult := UTF8.Encode(message);
     if encodeResult.Success? {
       encodedMsg := encodeResult.value;
     }
-    var keyA :- UTF8.Encode("keyA");
-    var valA :- UTF8.Encode("valA");
+    var keyA :- expect UTF8.Encode("keyA");
+    var valA :- expect UTF8.Encode("valA");
     var encryptionContext := map[keyA := valA];
     assert Msg.ValidAAD(encryptionContext) by {
       // To prove ValidAAD, we need to reveal the definition of ValidAAD:
@@ -50,33 +50,27 @@ module IntegTestKMS {
       assert Msg.KVPairsLength(encryptionContext) < UINT16_LIMIT;
     }
     var e := Client.Encrypt(encodedMsg, cmm, Some(encryptionContext), None, None);
-    if e.Failure? {
-      return Failure("Bad encryption :( " + e.error + "\n");
-    }
+    expect e.Success?, "Bad encryption :( " + e.error + "\n";
 
     var d := Client.Decrypt(e.value, cmm);
-    if d.Failure? {
-      return Failure("bad decryption: " + d.error + "\n");
-    }
-    if UTF8.ValidUTF8Seq(d.value) {
-      res := UTF8.Decode(d.value);
-    } else {
-      return Failure("Could not decode Encryption output");
-    }
+    expect d.Success?, "bad decryption: " + d.error + "\n";
+
+    expect UTF8.ValidUTF8Seq(d.value), "Could not decode Encryption output";
+    res :- expect UTF8.Decode(d.value);
   }
 
-  method {:test} TestEndToEnd() returns (r: Result<()>) {
-    var namespace :- UTF8.Encode("namespace");
-    var name :- UTF8.Encode("MyKeyring");
+  method {:test} TestEndToEnd() {
+    var namespace :- expect UTF8.Encode("namespace");
+    var name :- expect UTF8.Encode("MyKeyring");
     var generatorStr := SHARED_TEST_KEY_ARN;
-    var _ :- Require(KMSUtils.ValidFormatCMK(generatorStr));
+    expect KMSUtils.ValidFormatCMK(generatorStr);
     var generator: KMSUtils.CustomerMasterKey := generatorStr;
     var clientSupplier := new KMSUtils.DefaultClientSupplier();
     var keyring := new KMSKeyringDef.KMSKeyring(clientSupplier, [], Some(generator), []);
     var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring);
 
     var message := "Hello, World!!";
-    var result :- EncryptDecryptTest(cmm, message);
-    r := RequireEqual(message, result);
+    var result := EncryptDecryptTest(cmm, message);
+    expect message == result;
   }
 }

test/Keyring/KMSKeyring.dfy

@@ -10,34 +10,34 @@ module TestKMSKeyring {
   import opened UInt = StandardLibrary.UInt
   import KMSKeyringDef
   import KMSUtils
-  method {:test} TestRegionParseValidInput() returns (r: Result<()>) {
+  method {:test} TestRegionParseValidInput() {
     var cmk := "arn:aws:kms:us-west-1:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f";
-    var _ :- Require(KMSUtils.ValidFormatCMK(cmk));
-    var res :- KMSKeyringDef.RegionFromKMSKeyARN(cmk);
-    r := RequireEqual("us-west-1", res);
+    expect KMSUtils.ValidFormatCMK(cmk);
+    var res :- expect KMSKeyringDef.RegionFromKMSKeyARN(cmk);
+    expect "us-west-1" == res;
   }
-  method {:test} TestRegionParseValidInputWildPartition() returns (r: Result<()>) {
+  method {:test} TestRegionParseValidInputWildPartition() {
     var cmk := "arn:xxx:kms:us-west-1:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f";
-    var _ :- Require(KMSUtils.ValidFormatCMK(cmk));
-    var res :- KMSKeyringDef.RegionFromKMSKeyARN(cmk);
-    r := RequireEqual("us-west-1", res);
+    expect KMSUtils.ValidFormatCMK(cmk);
+    var res :- expect KMSKeyringDef.RegionFromKMSKeyARN(cmk);
+    expect "us-west-1" == res;
   }
-  method {:test} TestRegionParseValidInputNoPartition() returns (r: Result<()>) {
+  method {:test} TestRegionParseValidInputNoPartition() {
     var cmk := "arn::kms:us-west-1:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f";
-    var _ :- Require(KMSUtils.ValidFormatCMK(cmk));
-    var res :- KMSKeyringDef.RegionFromKMSKeyARN(cmk);
-    r := RequireEqual("us-west-1", res);
+    expect KMSUtils.ValidFormatCMK(cmk);
+    var res :- expect KMSKeyringDef.RegionFromKMSKeyARN(cmk);
+    expect "us-west-1" == res;
   }
-  method {:test} TestRegionParseValidInputAliasArn() returns (r: Result<()>) {
+  method {:test} TestRegionParseValidInputAliasArn() {
     var cmk := "arn:aws:kms:us-west-1:658956600833:alias/EncryptDecrypt";
-    var _ :- Require(KMSUtils.ValidFormatCMK(cmk));
-    var res :- KMSKeyringDef.RegionFromKMSKeyARN(cmk);
-    r := RequireEqual("us-west-1", res);
+    expect KMSUtils.ValidFormatCMK(cmk);
+    var res :- expect KMSKeyringDef.RegionFromKMSKeyARN(cmk);
+    expect "us-west-1" == res;
   }
-  method {:test} TestRegionParseBadInputAlias() returns (r: Result<()>) {
+  method {:test} TestRegionParseBadInputAlias() {
     var cmk := "alias/EncryptDecrypt";
-    var _ :- Require(KMSUtils.ValidFormatCMK(cmk));
+    expect KMSUtils.ValidFormatCMK(cmk);
     var res := KMSKeyringDef.RegionFromKMSKeyARN(cmk);
-    r := Require(res.Failure? && res.error == "Malformed ARN");
+    expect res.Failure? && res.error == "Malformed ARN";
   }
 }

test/SDK/Client.dfy

@@ -23,12 +23,12 @@ module {:extern "TestClient"} TestClient {
   import UTF8
   import Base64
 
-  method EncryptDecryptTest(cmm: CMMDefs.CMM) returns (r: Result<()>)
+  method EncryptDecryptTest(cmm: CMMDefs.CMM)
     requires cmm.Valid()
   {
-    var msg :- UTF8.Encode("hello");
-    var keyA :- UTF8.Encode("keyA");
-    var valA :- UTF8.Encode("valA");
+    var msg :- expect UTF8.Encode("hello");
+    var keyA :- expect UTF8.Encode("keyA");
+    var valA :- expect UTF8.Encode("valA");
     var encryptionContext := map[keyA := valA];
     assert Msg.ValidAAD(encryptionContext) by {
       // To prove ValidAAD, we need to reveal the definition of ValidAAD:
@@ -43,21 +43,21 @@ module {:extern "TestClient"} TestClient {
       }
       assert Msg.KVPairsLength(encryptionContext) < UINT16_LIMIT;
     }
-    var e :- Client.Encrypt(msg, cmm, Some(encryptionContext), None, None);
+    var e :- expect Client.Encrypt(msg, cmm, Some(encryptionContext), None, None);
 
-    var d :- Client.Decrypt(e, cmm);
+    var d :- expect Client.Decrypt(e, cmm);
 
-    r := RequireEqual(msg, d);
+    expect msg == d;
   }
 
-  method {:test} HappyPath() returns (r: Result<()>) {
-    var namespace :- UTF8.Encode("namespace");
-    var name :- UTF8.Encode("MyKeyring");
+  method {:test} HappyPath() {
+    var namespace :- expect UTF8.Encode("namespace");
+    var name :- expect UTF8.Encode("MyKeyring");
 
     var ek, dk := RSA.GenerateKeyPair(2048, RSA.PKCS1);
     var keyring := new RawRSAKeyringDef.RawRSAKeyring(namespace, name, RSA.PaddingMode.PKCS1, Some(ek), Some(dk));
     var cmm := new DefaultCMMDef.DefaultCMM.OfKeyring(keyring);
 
-    r := EncryptDecryptTest(cmm);
+    EncryptDecryptTest(cmm);
   }
 }