Skip to content

Commit 268ffd7

Browse files
authored
chore(dafny): remove duplicate proof in kms keyring (#1526)
1 parent 7e0ed9e commit 268ffd7

File tree

1 file changed

+1
-12
lines changed
  • AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms

1 file changed

+1
-12
lines changed

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy

Lines changed: 1 addition & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -389,9 +389,7 @@ module AwsKmsKeyring {
389389
//# OnDecrypt MUST take [decryption materials]
390390
//# (../structures.md#decryption-materials) and a list of [encrypted data
391391
//# keys](../structures.md#encrypted-data-key) as input.
392-
method {:verify false} {:vcs_split_on_every_assert} OnDecrypt'(
393-
// TODO-HV-2-BLOCKER :: added verify false in order to unblock continuing work
394-
// remove before release.
392+
method {:vcs_split_on_every_assert} OnDecrypt'(
395393
input: Types.OnDecryptInput
396394
)
397395
returns (res: Result<Types.OnDecryptOutput, Types.Error>)
@@ -559,15 +557,6 @@ module AwsKmsKeyring {
559557
&& maybeWrappedMaterial.Success?
560558
&& KMS.IsValid_CiphertextType(maybeWrappedMaterial.value);
561559

562-
563-
assert exists edk | edk in edksToAttempt
564-
::
565-
&& var maybeWrappedMaterial :=
566-
EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, input.materials.algorithmSuite);
567-
&& maybeWrappedMaterial.Success?
568-
&& KMS.IsValid_CiphertextType(maybeWrappedMaterial.value);
569-
570-
571560
assert decryptClosure.Ensures(Last(attempts).input, Success(SealedDecryptionMaterials), DropLast(attempts));
572561
return Success(Types.OnDecryptOutput(
573562
materials := SealedDecryptionMaterials

0 commit comments

Comments
 (0)