format

aws · Oct 26, 2024 · 1fdf3f7 · 1fdf3f7
1 parent 0c46bb3
commit 1fdf3f7
Show file tree

Hide file tree

Showing 11 changed files with 43 additions and 43 deletions.
diff --git a/...ialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy b/...ialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy
@@ -76,7 +76,7 @@ module MaterialWrapping {
   // a set of material originally wrapped by `WrapMaterial`.
   trait {:termination false} GenerateAndWrapMaterial<T>
     extends ActionWithResult<GenerateAndWrapInput, GenerateAndWrapOutput<T>, Types.Error>
-    {
+  {
     method Invoke(input: GenerateAndWrapInput, ghost attemptsState: seq<ActionInvoke<GenerateAndWrapInput, Result<GenerateAndWrapOutput<T>, Types.Error>>>)
       returns (r: Result<GenerateAndWrapOutput<T>, Types.Error>)
       requires Invariant()
@@ -97,7 +97,7 @@ module MaterialWrapping {
 
   trait {:termination false} WrapMaterial<T>
     extends ActionWithResult<WrapInput, WrapOutput<T>, Types.Error>
-    {
+  {
     method Invoke(input: WrapInput, ghost attemptsState: seq<ActionInvoke<WrapInput, Result<WrapOutput<T>, Types.Error>>>)
       returns (r: Result<WrapOutput<T>, Types.Error>)
       requires Invariant()
@@ -116,7 +116,7 @@ module MaterialWrapping {
 
   trait {:termination false} UnwrapMaterial<T>
     extends ActionWithResult<UnwrapInput, UnwrapOutput<T>, Types.Error>
-    {
+  {
     method Invoke(input: UnwrapInput, ghost attemptsState: seq<ActionInvoke<UnwrapInput, Result<UnwrapOutput<T>, Types.Error>>>)
       returns (r: Result<UnwrapOutput<T>, Types.Error>)
       requires Invariant()

diff --git a/...rs/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy b/...rs/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy
@@ -36,7 +36,7 @@ module AwsKmsDiscoveryKeyring {
     //= type=implication
     //# MUST implement that [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface)
     extends Keyring.VerifiableInterface
-    {
+  {
     const client: KMS.IKMSClient
     const discoveryFilter: Option<Types.DiscoveryFilter>
     const grantTokens: KMS.GrantTokenList
@@ -312,7 +312,7 @@ module AwsKmsDiscoveryKeyring {
       bool,
       Types.Error
     >
-    {
+  {
     const discoveryFilter: Option<Types.DiscoveryFilter>
     constructor(
       discoveryFilter: Option<Types.DiscoveryFilter>
@@ -398,9 +398,9 @@ module AwsKmsDiscoveryKeyring {
     extends DeterministicActionWithResult<
       Types.EncryptedDataKey,
       seq<AwsKmsEdkHelper>,
-          Types.Error
+      Types.Error
     >
-    {
+  {
     constructor() {}
 
     predicate Ensures(
@@ -454,7 +454,7 @@ module AwsKmsDiscoveryKeyring {
       AwsKmsEdkHelper,
       Materials.SealedDecryptionMaterials,
       Types.Error>
-    {
+  {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const client: KMS.IKMSClient
     const grantTokens: KMS.GrantTokenList

diff --git a/...oviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy b/...oviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy
@@ -48,7 +48,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
   //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface)
   class AwsKmsEcdhKeyring
     extends Keyring.VerifiableInterface
-    {
+  {
     const client: KMS.IKMSClient
     const senderKmsKeyId: Option<AwsKmsIdentifierString>
     const senderPublicKey: Option<KMS.PublicKeyType>
@@ -469,7 +469,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
       Types.EncryptedDataKey,
       Materials.SealedDecryptionMaterials,
       Types.Error>
-    {
+  {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
     const recipientPublicKey: seq<uint8>
@@ -655,7 +655,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
 
   class OnDecryptEcdhDataKeyFilter
     extends DeterministicActionWithResult<Types.EncryptedDataKey, bool, Types.Error>
-    {
+  {
     const keyAgreementScheme: Types.KmsEcdhStaticConfigurations
     const compressedRecipientPublicKey: seq<uint8>
     const compressedSenderPublicKey: seq<uint8>
@@ -685,7 +685,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
         ==>
           (edk.keyProviderId == KMS_ECDH_PROVIDER_ID ||
            edk.keyProviderId == RAW_ECDH_PROVIDER_ID)
-           && UTF8.ValidUTF8Seq(edk.keyProviderId)
+          && UTF8.ValidUTF8Seq(edk.keyProviderId)
       )
     }
 

diff --git a/...dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/...dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy
@@ -107,7 +107,7 @@ module AwsKmsHierarchicalKeyring {
   //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface)
   class AwsKmsHierarchicalKeyring
     extends Keyring.VerifiableInterface
-    {
+  {
     const branchKeyId: Option<string>
     const branchKeyIdSupplier: Option<Types.IBranchKeyIdSupplier>
     const keyStore: KeyStore.IKeyStoreClient
@@ -602,7 +602,7 @@ module AwsKmsHierarchicalKeyring {
 
   class OnDecryptHierarchyEncryptedDataKeyFilter
     extends DeterministicActionWithResult<Types.EncryptedDataKey, bool, Types.Error>
-    {
+  {
     const branchKeyId: string
 
     constructor(
@@ -658,7 +658,7 @@ module AwsKmsHierarchicalKeyring {
       Types.EncryptedDataKey,
       Materials.SealedDecryptionMaterials,
       Types.Error>
-    {
+  {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const keyStore: KeyStore.IKeyStoreClient
     const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
@@ -931,7 +931,7 @@ module AwsKmsHierarchicalKeyring {
 
   class KmsHierarchyUnwrapKeyMaterial
     extends MaterialWrapping.UnwrapMaterial<HierarchyUnwrapInfo>
-    {
+  {
     const branchKey: seq<uint8>
     const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes
     const branchKeyVersionAsBytes: seq<uint8>
@@ -1068,7 +1068,7 @@ module AwsKmsHierarchicalKeyring {
 
   class KmsHierarchyGenerateAndWrapKeyMaterial
     extends MaterialWrapping.GenerateAndWrapMaterial<HierarchyWrapInfo>
-    {
+  {
     const branchKey: seq<uint8>
     const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes
     const branchKeyVersionAsBytes: seq<uint8>
@@ -1160,7 +1160,7 @@ module AwsKmsHierarchicalKeyring {
 
   class KmsHierarchyWrapKeyMaterial
     extends MaterialWrapping.WrapMaterial<HierarchyWrapInfo>
-    {
+  {
     const branchKey: seq<uint8>
     const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes
     const branchKeyVersionAsBytes: seq<uint8>

diff --git a/...alProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/...alProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy
@@ -39,7 +39,7 @@ module AwsKmsKeyring {
   //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface)
   class AwsKmsKeyring
     extends Keyring.VerifiableInterface
-    {
+  {
     const client: KMS.IKMSClient
     const awsKmsKey: AwsKmsIdentifierString
     const awsKmsArn: AwsKmsIdentifier
@@ -582,7 +582,7 @@ module AwsKmsKeyring {
 
   class OnDecryptEncryptedDataKeyFilter
     extends DeterministicActionWithResult<Types.EncryptedDataKey, bool, Types.Error>
-    {
+  {
     const awsKmsKey: AwsKmsIdentifierString
 
     constructor(awsKmsKey: AwsKmsIdentifierString) {
@@ -636,7 +636,7 @@ module AwsKmsKeyring {
       Types.EncryptedDataKey,
       Materials.SealedDecryptionMaterials,
       Types.Error>
-    {
+  {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const client: KMS.IKMSClient
     const awsKmsKey: AwsKmsIdentifierString
@@ -752,7 +752,7 @@ module AwsKmsKeyring {
 
   class KmsUnwrapKeyMaterial
     extends MaterialWrapping.UnwrapMaterial<KmsUnwrapInfo>
-    {
+  {
     const client: KMS.IKMSClient
     const awsKmsKey: AwsKmsIdentifierString
     const grantTokens: KMS.GrantTokenList
@@ -856,7 +856,7 @@ module AwsKmsKeyring {
 
   class KmsGenerateAndWrapKeyMaterial
     extends MaterialWrapping.GenerateAndWrapMaterial<KmsWrapInfo>
-    {
+  {
     const client: KMS.IKMSClient
     const awsKmsKey: AwsKmsIdentifierString
     const grantTokens: KMS.GrantTokenList
@@ -1002,7 +1002,7 @@ module AwsKmsKeyring {
 
   class KmsWrapKeyMaterial
     extends MaterialWrapping.WrapMaterial<KmsWrapInfo>
-    {
+  {
     const client: KMS.IKMSClient
     const awsKmsKey: AwsKmsIdentifierString
     const grantTokens: KMS.GrantTokenList

diff --git a/...dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy b/...dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy
@@ -38,7 +38,7 @@ module AwsKmsMrkDiscoveryKeyring {
     //# MUST implement that [AWS Encryption SDK Keyring interface](../keyring-
     //# interface.md#interface)
     extends Keyring.VerifiableInterface
-    {
+  {
     const client: KMS.IKMSClient
     const discoveryFilter: Option<Types.DiscoveryFilter>
     const grantTokens: KMS.GrantTokenList
@@ -347,9 +347,9 @@ module AwsKmsMrkDiscoveryKeyring {
     extends DeterministicActionWithResult<
       Types.EncryptedDataKey,
       seq<AwsKmsEdkHelper>,
-          Types.Error
+      Types.Error
     >
-    {
+  {
     const region: string
     const discoveryFilter: Option<Types.DiscoveryFilter>
     constructor(
@@ -430,7 +430,7 @@ module AwsKmsMrkDiscoveryKeyring {
       AwsKmsEdkHelper,
       Materials.SealedDecryptionMaterials,
       Types.Error>
-    {
+  {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const client: KMS.IKMSClient
     const region : string

diff --git a/...roviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy b/...roviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy
@@ -38,7 +38,7 @@ module AwsKmsMrkKeyring {
   //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface)
   class AwsKmsMrkKeyring
     extends Keyring.VerifiableInterface
-    {
+  {
 
     const client: KMS.IKMSClient
     const awsKmsKey: AwsKmsIdentifierString
@@ -565,7 +565,7 @@ module AwsKmsMrkKeyring {
       Types.EncryptedDataKey,
       Materials.SealedDecryptionMaterials,
       Types.Error>
-    {
+  {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const client: KMS.IKMSClient
     const awsKmsKey: AwsKmsIdentifierString

diff --git a/...roviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy b/...roviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsRsaKeyring.dfy
@@ -41,7 +41,7 @@ module AwsKmsRsaKeyring {
 
   class AwsKmsRsaKeyring
     extends Keyring.VerifiableInterface
-    {
+  {
     const client: Option<KMS.IKMSClient>
     const grantTokens: KMS.GrantTokenList
     const awsKmsKey: AwsArnParsing.AwsKmsIdentifierString
@@ -342,7 +342,7 @@ module AwsKmsRsaKeyring {
       Types.EncryptedDataKey,
       Materials.SealedDecryptionMaterials,
       Types.Error>
-    {
+  {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const client: KMS.IKMSClient
     const awsKmsKey: AwsArnParsing.AwsKmsIdentifierString
@@ -456,7 +456,7 @@ module AwsKmsRsaKeyring {
 
   class KmsRsaGenerateAndWrapKeyMaterial
     extends MaterialWrapping.GenerateAndWrapMaterial<KmsRsaWrapInfo>
-    {
+  {
     const publicKey: seq<uint8>
     const paddingScheme: KMS.EncryptionAlgorithmSpec
     const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
@@ -538,7 +538,7 @@ module AwsKmsRsaKeyring {
 
   class KmsRsaWrapKeyMaterial
     extends MaterialWrapping.WrapMaterial<KmsRsaWrapInfo>
-    {
+  {
     const publicKey: seq<uint8>
     const paddingScheme: KMS.EncryptionAlgorithmSpec
     const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
@@ -616,7 +616,7 @@ module AwsKmsRsaKeyring {
 
   class KmsRsaUnwrapKeyMaterial
     extends MaterialWrapping.UnwrapMaterial<KmsRsaUnwrapInfo>
-    {
+  {
     const client: KMS.IKMSClient
     const awsKmsKey: AwsArnParsing.AwsKmsIdentifierString
     const paddingScheme: KMS.EncryptionAlgorithmSpec

diff --git a/...icMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy b/...icMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy
@@ -19,7 +19,7 @@ module MultiKeyring {
     extends
       Keyring.VerifiableInterface,
       Types.IKeyring
-      {
+  {
 
     predicate ValidState()
       ensures ValidState() ==> History in Modifies

diff --git a/...MaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy b/...MaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy
@@ -65,7 +65,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring {
   //# MUST implement the [AWS Encryption SDK Keyring interface](../keyring-interface.md#interface)
   class RawEcdhKeyring
     extends Keyring.VerifiableInterface
-    {
+  {
     const senderPrivateKey: PrimitiveTypes.ECCPrivateKey
     const senderPublicKey: PrimitiveTypes.ECCPublicKey
     const recipientPublicKey: PrimitiveTypes.ECCPublicKey
@@ -415,7 +415,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring {
 
   class OnDecryptEcdhDataKeyFilter
     extends DeterministicActionWithResult<Types.EncryptedDataKey, bool, Types.Error>
-    {
+  {
     const keyAgreementScheme: Types.RawEcdhStaticConfigurations
     const compressedRecipientPublicKey: seq<uint8>
     const compressedSenderPublicKey: seq<uint8>
@@ -513,7 +513,7 @@ module {:options "/functionSyntax:4" } RawECDHKeyring {
       Types.EncryptedDataKey,
       Materials.SealedDecryptionMaterials,
       Types.Error>
-    {
+  {
     const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
     const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
     const senderPublicKey: seq<uint8>

diff --git a/StandardLibrary/src/Actions.dfy b/StandardLibrary/src/Actions.dfy
@@ -15,7 +15,7 @@ module Actions {
    * and return results of type R.
    */
   trait {:termination false} Action<A, R>
-    {
+  {
     /*
      * Contains the implementation of the given action
      */
@@ -58,7 +58,7 @@ module Actions {
    */
   trait {:termination false} ActionWithResult<A, R, E>
     extends Action<A, Result<R, E>>
-    {
+  {
     method Invoke(a: A, ghost attemptsState: seq<ActionInvoke<A, Result<R, E>>>)
       returns (r: Result<R, E>)
       requires Invariant()
@@ -70,7 +70,7 @@ module Actions {
   }
 
   trait {:termination false} DeterministicAction<A, R>
-    {
+  {
     /*
      * Contains the implementation of the given deterministic action
      */
@@ -92,7 +92,7 @@ module Actions {
    */
   trait {:termination false} DeterministicActionWithResult<A, R, E>
     extends DeterministicAction<A, Result<R, E>>
-    {
+  {
     method Invoke(a: A)
       returns (r: Result<R, E>)
       ensures Ensures(a, r)