chore: remove case-based if statement (#630)

Remove a case-based if statement, as it caused errors about non-determinism. Reduce resource use to fix a verification failure along the way.
aws · Aug 23, 2024 · 66f30ed · 66f30ed
1 parent f12fe5b
commit 66f30ed
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 8 deletions.
diff --git a/...MaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy b/...MaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawECDHKeyring.dfy
@@ -603,21 +603,24 @@ module {:options "/functionSyntax:4" } RawECDHKeyring {
 
       var sharedSecretPublicKey: seq<uint8>;
       var sharedSecretPrivateKey: seq<uint8>;
-      if {
-        case this.keyAgreementScheme.PublicKeyDiscovery? =>
+      match this.keyAgreementScheme {
+        case PublicKeyDiscovery(publicKeyDiscovery) => {
           sharedSecretPublicKey := senderPublicKey;
-          sharedSecretPrivateKey := this.keyAgreementScheme.PublicKeyDiscovery.recipientStaticPrivateKey;
-        case this.keyAgreementScheme.RawPrivateKeyToStaticPublicKey? =>
-          sharedSecretPrivateKey := this.keyAgreementScheme.RawPrivateKeyToStaticPublicKey.senderStaticPrivateKey;
-          if this.keyAgreementScheme.RawPrivateKeyToStaticPublicKey.recipientPublicKey == recipientPublicKey {
+          sharedSecretPrivateKey := publicKeyDiscovery.recipientStaticPrivateKey;
+        }
+        case RawPrivateKeyToStaticPublicKey(rawPrivateKeyToStaticPublicKey) => {
+          sharedSecretPrivateKey := rawPrivateKeyToStaticPublicKey.senderStaticPrivateKey;
+          if rawPrivateKeyToStaticPublicKey.recipientPublicKey == recipientPublicKey {
             sharedSecretPublicKey := recipientPublicKey;
           } else {
             sharedSecretPublicKey := senderPublicKey;
           }
-        case this.keyAgreementScheme.EphemeralPrivateKeyToStaticPublicKey? =>
+        }
+        case EphemeralPrivateKeyToStaticPublicKey(_) => {
           //= aws-encryption-sdk-specification/framework/key-agreement-schemas.md#ephemeralprivatekeytostaticpublickey
           //# On decrypt, the keyring MUST fail.
           return Failure(E("EphemeralPrivateKeyToStaticPublicKey Not allowed on decrypt"));
+        }
       }
 
       var _ :- ValidatePublicKey(

diff --git a/AwsCryptographyPrimitives/test/TestECDH.dfy b/AwsCryptographyPrimitives/test/TestECDH.dfy
@@ -466,7 +466,7 @@ module TestECDH {
     for i := 0 to |curves|
     {
       var curve := curves[i];
-      var originalPublicKey := derX509PublicKeys[i];
+      var originalPublicKey := expectLooseHexString(derX509PublicKeys[i]);
       var publicKeyBytes := HexStrings.FromHexString(originalPublicKey);
       var compressedKey := expectLooseHexString(compressedKeys[i]);
       var compressedKeyBytes := HexStrings.FromHexString(compressedKey);