Pre commit hook trailing whitespace (#283)

* chore: Add pre-commit hook to disallow trailing whitespace

* Remove trailing whitespace

All changes in this commit come from running the tailing-whitespace pre-commit hook.

Author: RustanLeino

.pre-commit-config.yaml

@@ -0,0 +1,5 @@
+repos:
+-   repo: https://github.com/pre-commit/pre-commit-hooks
+    rev: v2.2.3  # Use the ref you want to point at
+    hooks:
+    -   id: trailing-whitespace

CODE_OF_CONDUCT.md

@@ -1,4 +1,4 @@
 ## Code of Conduct
-This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct). 
-For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact 
+This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct).
+For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact
 [email protected] with any additional questions or comments.

CONTRIBUTING.md

@@ -1,17 +1,17 @@
 # Contributing Guidelines
 
-Thank you for your interest in contributing to our project. Whether it's a bug report, new feature, correction, or additional 
+Thank you for your interest in contributing to our project. Whether it's a bug report, new feature, correction, or additional
 documentation, we greatly value feedback and contributions from our community.
 
-Please read through this document before submitting any issues or pull requests to ensure we have all the necessary 
+Please read through this document before submitting any issues or pull requests to ensure we have all the necessary
 information to effectively respond to your bug report or contribution.
 
 
 ## Reporting Bugs/Feature Requests
 
 We welcome you to use the GitHub issue tracker to report bugs or suggest features.
 
-When filing an issue, please check [existing open](https://github.com/awslabs/aws-encryption-sdk-dafny/issues), or [recently closed](https://github.com/awslabs/aws-encryption-sdk-dafny/issues?utf8=%E2%9C%93&q=is%3Aissue%20is%3Aclosed%20), issues to make sure somebody else hasn't already 
+When filing an issue, please check [existing open](https://github.com/awslabs/aws-encryption-sdk-dafny/issues), or [recently closed](https://github.com/awslabs/aws-encryption-sdk-dafny/issues?utf8=%E2%9C%93&q=is%3Aissue%20is%3Aclosed%20), issues to make sure somebody else hasn't already
 reported the issue. Please try to include as much information as you can. Details like these are incredibly useful:
 
 * A reproducible test case or series of steps
@@ -41,17 +41,17 @@ To send us a pull request, please:
    the resulting commit title and message must adhere to conventional commits.
 6. Pay attention to any automated CI failures reported in the pull request, and stay involved in the conversation.
 
-GitHub provides additional document on [forking a repository](https://help.github.com/articles/fork-a-repo/) and 
+GitHub provides additional document on [forking a repository](https://help.github.com/articles/fork-a-repo/) and
 [creating a pull request](https://help.github.com/articles/creating-a-pull-request/).
 
 
 ## Finding contributions to work on
-Looking at the existing issues is a great way to find something to contribute on. As our projects, by default, use the default GitHub issue labels (enhancement/bug/duplicate/help wanted/invalid/question/wontfix), looking at any ['help wanted'](https://github.com/awslabs/aws-encryption-sdk-dafny/labels/help%20wanted) issues is a great place to start. 
+Looking at the existing issues is a great way to find something to contribute on. As our projects, by default, use the default GitHub issue labels (enhancement/bug/duplicate/help wanted/invalid/question/wontfix), looking at any ['help wanted'](https://github.com/awslabs/aws-encryption-sdk-dafny/labels/help%20wanted) issues is a great place to start.
 
 
 ## Code of Conduct
-This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct). 
-For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact 
+This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct).
+For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact
 [email protected] with any additional questions or comments.
 
 

Dockerfile

@@ -1,5 +1,5 @@
 FROM ubuntu:18.04
- 
+
 USER root
 
 ENV DEBIAN_FRONTEND=noninteractive

NOTICE

@@ -1,2 +1,2 @@
 AWS Encryption SDK Dafny
-Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved. 
+Copyright 2019 Amazon.com, Inc. or its affiliates. All Rights Reserved.

lib/.gitignore

@@ -1,5 +1,5 @@
 # ignore all files in this dir...
 *
- 
+
 # ... except for this one.
 !.gitignore

src/AWSEncryptionSDK.csproj

@@ -46,7 +46,7 @@
     <DafnySource Include="Util/UTF8.dfy" />
     <DafnySource Include="Util/Sets.dfy" />
   </ItemGroup>
-  
+
   <ItemGroup>
     <PackageReference Include="dafny.msbuild" Version="1.0.0" />
     <PackageReference Include="AWSSDK.Core" Version="3.3.104.1" />

src/Crypto/HKDF/HKDF.dfy

@@ -37,22 +37,22 @@ module HKDF {
   }
 
   // T is relational since the external hashMethod hmac.GetKey() ensures that the input and output of the hash method are in the relation hmac.HashSignature
-  // T depends on Ti and Ti depends on hmac.HashSignature 
+  // T depends on Ti and Ti depends on hmac.HashSignature
   predicate T(hmac: HMac, info: seq<uint8>, n: nat, res: seq<uint8>)
-    requires 0 <= n < 256	
+    requires 0 <= n < 256
     decreases n
-  {	
-    if n == 0 then 
+  {
+    if n == 0 then
       [] == res
-    else 
-      exists prev1, prev2 :: T(hmac, info, n-1, prev1) && Ti(hmac, info, n, prev2) && prev1 + prev2 == res	
+    else
+      exists prev1, prev2 :: T(hmac, info, n-1, prev1) && Ti(hmac, info, n, prev2) && prev1 + prev2 == res
   }
 
   predicate Ti(hmac: HMac, info: seq<uint8>, n: nat, res: seq<uint8>)
     requires 0 <= n < 256
     decreases n, 1
   {
-    if n == 0 then 
+    if n == 0 then
       res == []
     else
       exists prev :: PreTi(hmac, info, n, prev) &&  hmac.HashSignature(prev, res)
@@ -111,12 +111,12 @@ module HKDF {
       hmac.Update(t_prev);
       hmac.Update(info);
       hmac.Update([i as uint8]);
-      assert hmac.GetInputSoFar() == t_prev + info + [i as uint8];  
+      assert hmac.GetInputSoFar() == t_prev + info + [i as uint8];
 
       // Add additional verification for T(n): github.com/awslabs/aws-encryption-sdk-dafny/issues/177
-      t_prev := hmac.GetResult(); 
+      t_prev := hmac.GetResult();
       // t_n == T(i - 1)
-      assert T(hmac, info, i - 1, t_n); 
+      assert T(hmac, info, i - 1, t_n);
       assert Ti(hmac, info, i, t_prev) ;
 
       t_n := t_n + t_prev;

src/KMS/KMSUtils.dfy

@@ -33,7 +33,7 @@ module {:extern "KMSUtils"} KMSUtils {
     var components := Split(cmk, ':');
     UTF8.IsASCIIString(cmk) && 0 < |cmk| <= 2048 && |components| == 6 && components[0] == "arn" && components[2] == "kms" && Split(components[5], '/')[0] == "alias"
   }
-  
+
   type GrantToken = s: string | 0 < |s| <= 8192 witness "witness"
 
   datatype ResponseMetadata = ResponseMetadata(metadata: map<string, string>, requestID: string)

src/SDK/EncryptionContext.dfy

@@ -191,7 +191,7 @@ module {:extern "EncryptionContext"} EncryptionContext {
     } else if |encryptionContext| >= UINT16_LIMIT {
       return false;
     }
-    
+
     // Iterating through a map isn't feasbile in dafny for large maps, so instead
     // convert the map to a sequence of key pairs and iterate through the sequence
     var keys: seq<UTF8.ValidUTF8Bytes> := Sets.ComputeSetToOrderedSequence<uint8>(encryptionContext.Keys, UInt.UInt8Less);

src/SDK/Keyring/Defs.dfy

@@ -20,7 +20,7 @@ module {:extern "KeyringDefs"} KeyringDefs {
       ensures Valid()
       ensures res.Success? ==>
           && materials.encryptionContext == res.value.encryptionContext
-          && materials.algorithmSuiteID == res.value.algorithmSuiteID 
+          && materials.algorithmSuiteID == res.value.algorithmSuiteID
           && (materials.plaintextDataKey.Some? ==> res.value.plaintextDataKey == materials.plaintextDataKey)
           && materials.keyringTrace <= res.value.keyringTrace
           && materials.encryptedDataKeys <= res.value.encryptedDataKeys

src/SDK/Keyring/KMSKeyring.dfy

@@ -64,9 +64,9 @@ module {:extern "KMSKeyringDef"} KMSKeyringDef {
       requires |materials.encryptedDataKeys| == 0
       requires !isDiscovery
       ensures Valid()
-      ensures res.Success? ==> 
+      ensures res.Success? ==>
           && materials.encryptionContext == res.value.encryptionContext
-          && materials.algorithmSuiteID == res.value.algorithmSuiteID 
+          && materials.algorithmSuiteID == res.value.algorithmSuiteID
           && res.value.plaintextDataKey.Some?
           && materials.keyringTrace <= res.value.keyringTrace
           && materials.encryptedDataKeys <= res.value.encryptedDataKeys
@@ -106,9 +106,9 @@ module {:extern "KMSKeyringDef"} KMSKeyringDef {
     method OnEncrypt(materials: Mat.ValidEncryptionMaterials) returns (res: Result<Mat.ValidEncryptionMaterials>)
       requires Valid()
       ensures Valid()
-      ensures res.Success? ==> 
+      ensures res.Success? ==>
           && materials.encryptionContext == res.value.encryptionContext
-          && materials.algorithmSuiteID == res.value.algorithmSuiteID 
+          && materials.algorithmSuiteID == res.value.algorithmSuiteID
           && (materials.plaintextDataKey.Some? ==> res.value.plaintextDataKey == materials.plaintextDataKey)
           && materials.keyringTrace <= res.value.keyringTrace
           && materials.encryptedDataKeys <= res.value.encryptedDataKeys
@@ -128,7 +128,7 @@ module {:extern "KMSKeyringDef"} KMSKeyringDef {
           resultMaterials :- Generate(materials);
           assert resultMaterials.plaintextDataKey.Some?;
         } else {
-          resultMaterials := materials; 
+          resultMaterials := materials;
           encryptCMKs := encryptCMKs + [generator.get];
         }
       } else {
@@ -138,7 +138,7 @@ module {:extern "KMSKeyringDef"} KMSKeyringDef {
       assert materials.plaintextDataKey.Some? ==> resultMaterials.plaintextDataKey == materials.plaintextDataKey;
 
       var i := 0;
-      while i < |encryptCMKs| 
+      while i < |encryptCMKs|
           invariant resultMaterials.plaintextDataKey.Some?
           invariant materials.encryptionContext == resultMaterials.encryptionContext
           invariant materials.algorithmSuiteID == resultMaterials.algorithmSuiteID

src/SDK/Keyring/MultiKeyring.dfy

@@ -46,9 +46,9 @@ module {:extern "MultiKeyringDef"} MultiKeyringDef {
         method OnEncrypt(materials: Materials.ValidEncryptionMaterials) returns (res: Result<Materials.ValidEncryptionMaterials>)
             requires Valid()
             ensures Valid()
-            ensures res.Success? ==> 
+            ensures res.Success? ==>
                     && materials.encryptionContext == res.value.encryptionContext
-                    && materials.algorithmSuiteID == res.value.algorithmSuiteID 
+                    && materials.algorithmSuiteID == res.value.algorithmSuiteID
                     && (materials.plaintextDataKey.Some? ==> res.value.plaintextDataKey == materials.plaintextDataKey)
                     && materials.keyringTrace <= res.value.keyringTrace
                     && materials.encryptedDataKeys <= res.value.encryptedDataKeys
@@ -74,7 +74,7 @@ module {:extern "MultiKeyringDef"} MultiKeyringDef {
                 invariant materials.keyringTrace <= resultMaterials.keyringTrace
                 invariant materials.encryptedDataKeys <= resultMaterials.encryptedDataKeys
                 invariant materials.signingKey == resultMaterials.signingKey
-                decreases |children| - i 
+                decreases |children| - i
             {
                 resultMaterials :- children[i].OnEncrypt(resultMaterials);
                 i := i + 1;
@@ -108,9 +108,9 @@ module {:extern "MultiKeyringDef"} MultiKeyringDef {
             }
             var i := 0;
             while i < |children|
-                invariant res.Success? ==> 
+                invariant res.Success? ==>
                         && materials.encryptionContext == res.value.encryptionContext
-                        && materials.algorithmSuiteID == res.value.algorithmSuiteID 
+                        && materials.algorithmSuiteID == res.value.algorithmSuiteID
                         && (materials.plaintextDataKey.Some? ==> res.value.plaintextDataKey == materials.plaintextDataKey)
                         && materials.keyringTrace <= res.value.keyringTrace
                         && materials.verificationKey == res.value.verificationKey

src/SDK/Keyring/RawAESKeyring.dfy

@@ -101,9 +101,9 @@ module {:extern "RawAESKeyringDef"} RawAESKeyringDef {
     method OnEncrypt(materials: Mat.ValidEncryptionMaterials) returns (res: Result<Mat.ValidEncryptionMaterials>)
       // Keyring Trait conditions
       requires Valid()
-      ensures res.Success? ==> 
+      ensures res.Success? ==>
         && materials.encryptionContext == res.value.encryptionContext
-        && materials.algorithmSuiteID == res.value.algorithmSuiteID 
+        && materials.algorithmSuiteID == res.value.algorithmSuiteID
         && (materials.plaintextDataKey.Some? ==> res.value.plaintextDataKey == materials.plaintextDataKey)
         && materials.keyringTrace <= res.value.keyringTrace
         && materials.encryptedDataKeys <= res.value.encryptedDataKeys
@@ -197,7 +197,7 @@ module {:extern "RawAESKeyringDef"} RawAESKeyringDef {
         && AESEncryption.PlaintextDecryptedWithAAD(res.value.plaintextDataKey.get, EncryptionContext.MapToSeq(materials.encryptionContext))
 
       // KeyringTrace generated as expected
-      ensures res.Success? && materials.plaintextDataKey.None? && res.value.plaintextDataKey.Some? ==> 
+      ensures res.Success? && materials.plaintextDataKey.None? && res.value.plaintextDataKey.Some? ==>
           |res.value.keyringTrace| == |materials.keyringTrace| + 1 && res.value.keyringTrace[|materials.keyringTrace|] == DecryptTraceEntry()
 
       // If attempts to decrypt an EDK and the input EC cannot be serialized, return a Failure
@@ -221,7 +221,7 @@ module {:extern "RawAESKeyringDef"} RawAESKeyringDef {
           var _ :- Serialize.SerializeKVPairs(wr, materials.encryptionContext);
           var aad := wr.GetDataWritten();
           assert aad == EncryptionContext.MapToSeq(materials.encryptionContext);
-          
+
           var iv := GetIvFromProvInfo(edks[i].providerInfo);
           var encryptionOutput := DeserializeEDKCiphertext(edks[i].ciphertext, wrappingAlgorithm.tagLen as nat);
           var ptKey :- AESEncryption.AESDecrypt(wrappingAlgorithm, wrappingKey, encryptionOutput.cipherText, encryptionOutput.authTag, iv, aad);

src/SDK/Keyring/RawRSAKeyring.dfy

@@ -74,9 +74,9 @@ module {:extern "RawRSAKeyringDef"} RawRSAKeyringDef {
       requires Valid()
       // NOTE: encryptionContext is intentionally unused
       ensures publicKey.None? ==> res.Failure?
-      ensures res.Success? ==> 
+      ensures res.Success? ==>
         && materials.encryptionContext == res.value.encryptionContext
-        && materials.algorithmSuiteID == res.value.algorithmSuiteID 
+        && materials.algorithmSuiteID == res.value.algorithmSuiteID
         && (materials.plaintextDataKey.Some? ==> res.value.plaintextDataKey == materials.plaintextDataKey)
         && materials.keyringTrace <= res.value.keyringTrace
         && materials.encryptedDataKeys <= res.value.encryptedDataKeys

src/SDK/Materials.dfy

@@ -97,15 +97,15 @@ module {:extern "Materials"} Materials {
 
     static function method WithoutDataKeys(encryptionContext: EncryptionContext.Map,
                                            algorithmSuiteID: AlgorithmSuite.ID,
-                                           signingKey: Option<seq<uint8>>): ValidEncryptionMaterials 
+                                           signingKey: Option<seq<uint8>>): ValidEncryptionMaterials
       requires algorithmSuiteID.SignatureType().Some? ==> signingKey.Some?
     {
       var m := EncryptionMaterials(encryptionContext, algorithmSuiteID, None, [], [], signingKey);
       assert m.Valid();
       m
     }
 
-    function method WithKeys(newPlaintextDataKey: Option<seq<uint8>>, 
+    function method WithKeys(newPlaintextDataKey: Option<seq<uint8>>,
                              newEncryptedDataKeys: seq<ValidEncryptedDataKey>,
                              newTraceEntries: seq<KeyringTraceEntry>): (res: ValidEncryptionMaterials)
       requires Valid()
@@ -117,13 +117,13 @@ module {:extern "Materials"} Materials {
       requires (newPlaintextDataKey == this.plaintextDataKey) ==> (forall entry :: entry in newTraceEntries ==> !IsGenerateTraceEntry(entry))
       requires |Filter(newTraceEntries, IsEncryptTraceEntry)| == |newEncryptedDataKeys|
       ensures this.encryptionContext == res.encryptionContext
-      ensures this.algorithmSuiteID == res.algorithmSuiteID 
+      ensures this.algorithmSuiteID == res.algorithmSuiteID
       ensures newPlaintextDataKey == res.plaintextDataKey
       ensures this.keyringTrace + newTraceEntries == res.keyringTrace
       ensures this.encryptedDataKeys + newEncryptedDataKeys == res.encryptedDataKeys
       ensures this.signingKey == res.signingKey
     {
-        var r := this.(plaintextDataKey := newPlaintextDataKey, 
+        var r := this.(plaintextDataKey := newPlaintextDataKey,
                        encryptedDataKeys := encryptedDataKeys + newEncryptedDataKeys,
                        keyringTrace := keyringTrace + newTraceEntries);
         FilterIsDistributive(keyringTrace, newTraceEntries, IsEncryptTraceEntry);
@@ -155,7 +155,7 @@ module {:extern "Materials"} Materials {
 
     static function method WithoutPlaintextDataKey(encryptionContext: EncryptionContext.Map,
                                                    algorithmSuiteID: AlgorithmSuite.ID,
-                                                   verificationKey: Option<seq<uint8>>): ValidDecryptionMaterials 
+                                                   verificationKey: Option<seq<uint8>>): ValidDecryptionMaterials
       requires algorithmSuiteID.SignatureType().Some? ==> verificationKey.Some?
     {
       var m := DecryptionMaterials(algorithmSuiteID, encryptionContext, None, verificationKey, []);
@@ -174,7 +174,7 @@ module {:extern "Materials"} Materials {
       ensures this.keyringTrace <= res.keyringTrace
       ensures this.verificationKey == res.verificationKey
     {
-      var m := this.(plaintextDataKey := Some(plaintextDataKey), 
+      var m := this.(plaintextDataKey := Some(plaintextDataKey),
                      keyringTrace := this.keyringTrace + newTraceEntries);
       assert m.Valid();
       m

src/StandardLibrary/Base64.dfy

@@ -172,7 +172,7 @@ module Base64 {
     if |b| == 0 then []
     else EncodeBlock(b[..3]) + EncodeRecursively(b[3..])
   }
-  
+
   lemma DecodeEncodeRecursively(s: seq<index>)
     requires |s| % 4 == 0
     ensures EncodeRecursively(DecodeRecursively(s)) == s

src/api/dotnet/Client.cs

@@ -20,15 +20,15 @@ public static MemoryStream Encrypt(EncryptRequest request) {
             STL.Result<ibyteseq> result = ESDKClient.__default.Encrypt(request.GetDafnyRequest());
             return DafnyFFI.MemoryStreamFromSequence(DafnyFFI.ExtractResult(result));
         }
-  
+
         // TODO: Proper documentation
         public static MemoryStream Decrypt(DecryptRequest request) {
             // TODO: Might need a lock here if ANYTHING in the Dafny runtime isn't threadsafe!
             STL.Result<ibyteseq> result = ESDKClient.__default.Decrypt(request.GetDafnyRequest());
-    
+
             return DafnyFFI.MemoryStreamFromSequence(DafnyFFI.ExtractResult(result));
         }
-  
+
         private static encryptioncontext ToDafnyEncryptionContext(Dictionary<string, string> encryptionContext)
         {
             IEnumerable<Pair<ibyteseq, ibyteseq>> e = encryptionContext.Select(entry
@@ -65,7 +65,7 @@ internal ESDKClient.EncryptRequest GetDafnyRequest() {
                 };
             }
         }
-        
+
         public class DecryptRequest {
             public MemoryStream message { get; set;}
             public CMM cmm { get; set;}