From 7d44c71ee2452781768ae4b32913f179cc56cf9d Mon Sep 17 00:00:00 2001
From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com>
Date: Tue, 13 Aug 2024 15:20:18 -0400
Subject: [PATCH] chore: add documentation to externs (#590)

* chore: add documentation to externs
---
 AwsCryptographyPrimitives/src/Digest.dfy    |  7 +++----
 AwsCryptographyPrimitives/src/ECDH.dfy      | 17 +++++++++++++++++
 AwsCryptographyPrimitives/src/Signature.dfy |  8 ++++++++
 3 files changed, 28 insertions(+), 4 deletions(-)

diff --git a/AwsCryptographyPrimitives/src/Digest.dfy b/AwsCryptographyPrimitives/src/Digest.dfy
index e97509c7a..b3ad11eb1 100644
--- a/AwsCryptographyPrimitives/src/Digest.dfy
+++ b/AwsCryptographyPrimitives/src/Digest.dfy
@@ -13,10 +13,9 @@ module Digest {
   function method Length(digestAlgorithm: Types.DigestAlgorithm): nat
   {
     match digestAlgorithm
-    case SHA_512 => 64
-    case SHA_384 => 48
-    case SHA_256 => 32
-    case SHA_1 => 20
+    case SHA_512() => 64
+    case SHA_384() => 48
+    case SHA_256() => 32
   }
 
   method Digest(input: Types.DigestInput)
diff --git a/AwsCryptographyPrimitives/src/ECDH.dfy b/AwsCryptographyPrimitives/src/ECDH.dfy
index acc3664dc..f099c92a6 100644
--- a/AwsCryptographyPrimitives/src/ECDH.dfy
+++ b/AwsCryptographyPrimitives/src/ECDH.dfy
@@ -107,37 +107,54 @@ module {:extern "ECDH"} ECDH {
                    ));
   }
 
+  // Generate an ECDH key pair
+  // Return the private key as UTF8 PEM-encoded Rfc5915 format,
+  // Return the public key as DER-encoded X.509 SubjectPublicKeyInfo bytes
   method {:extern "ECDH.KeyGeneration", "GenerateKeyPair"} ExternEccKeyGen(
     s: Types.ECDHCurveSpec
   ) returns (res: Result<EccKeyPair, Types.Error>)
     ensures res.Success? ==> 1 < |res.value.publicKey| <= 8192
 
+  // Given a private key, return the associated public key
+  // Input private key is in PEM format
+  // Output public key is DER-encoded X.509 SubjectPublicKeyInfo
   method {:extern "ECDH.ECCUtils", "GetPublicKey"} ExternGetPublicKeyFromPrivate(
     curveAlgorithm: Types.ECDHCurveSpec,
     privateKey: Types.ECCPrivateKey
   ) returns (res: Result<seq<uint8>, Types.Error>)
 
+  // Ensure that this public key follows 5.6.2.3.3 ECC Full Public-Key Validation Routine from
+  // https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-56Ar3.pdf#page=55
+  // Input public key is DER-encoded X.509 SubjectPublicKeyInfo bytes
+  // Result is never Success(false), it's either Success(true) or Failure()
   method {:extern "ECDH.ECCUtils", "ValidatePublicKey"} ExternValidatePublicKey(
     curveAlgorithm: Types.ECDHCurveSpec,
     publicKey: seq<uint8>
   ) returns (res: Result<bool, Types.Error>)
 
+  // Calculate a shared secret from the keys
+  // Private key is PEM formatted UTF8
+  // Input public key is DER-encoded X.509 SubjectPublicKeyInfo bytes
   method {:extern "ECDH.DeriveSharedSecret", "CalculateSharedSecret"} ExternDeriveSharedSecret(
     curveAlgorithm: Types.ECDHCurveSpec,
     privateKey: Types.ECCPrivateKey,
     publicKey: Types.ECCPublicKey
   ) returns (res: Result<seq<uint8>, Types.Error>)
 
+  // Convert DER-encoded X.509 SubjectPublicKeyInfo public key bytes to compressed X9.62 format
   method {:extern "ECDH.ECCUtils", "CompressPublicKey"} ExternCompressPublicKey(
     publicKey: seq<uint8>,
     curveAlgorithm: Types.ECDHCurveSpec
   ) returns (res: Result<seq<uint8>, Types.Error>)
 
+  // Convert X9.62 encoded public key bytes to DER-encoded X.509 SubjectPublicKeyInfo format
+  // input is not PEM-encoded
   method {:extern "ECDH.ECCUtils", "DecompressPublicKey"} ExternDecompressPublicKey(
     publicKey: seq<uint8>,
     curveAlgorithm: Types.ECDHCurveSpec
   ) returns (res: Result<seq<uint8>, Types.Error>)
 
+  // Ensure that this public key is DER-encoded X.509 SubjectPublicKeyInfo format
   method {:extern "ECDH.ECCUtils", "ParsePublicKey"} ExternParsePublicKey(
     publicKey: seq<uint8>
   ) returns (res: Result<seq<uint8>, Types.Error>)
diff --git a/AwsCryptographyPrimitives/src/Signature.dfy b/AwsCryptographyPrimitives/src/Signature.dfy
index b550b9fda..c87d33469 100644
--- a/AwsCryptographyPrimitives/src/Signature.dfy
+++ b/AwsCryptographyPrimitives/src/Signature.dfy
@@ -55,11 +55,16 @@ module {:extern "Signature"} Signature {
                    ));
   }
 
+  // Generate an ECDSA key pair
+  // Verification key, a.k.a public key, is in X9.62 compressed format
+  // Signing Key, a.k.a private key, is in DER-encoded
   method {:extern "Signature.ECDSA", "ExternKeyGen"} ExternKeyGen(
     s: Types.ECDSASignatureAlgorithm
   ) returns (res: Result<SignatureKeyPair, Types.Error>)
     ensures res.Success? ==> IsValidSignatureKeyPair(res.value)
 
+  // sign the message with the private key
+  // private signing key is DER-encoded
   method {:extern "Signature.ECDSA", "Sign"} Sign(
     s: Types.ECDSASignatureAlgorithm,
     key: seq<uint8>,
@@ -67,6 +72,9 @@ module {:extern "Signature"} Signature {
   ) returns (sig: Result<seq<uint8>, Types.Error>)
     ensures sig.Success? ==> IsSigned(key, msg, sig.value)
 
+  // Verify that these bytes created this signature
+  // Public verification key is DER-encoded X9.62 format
+  // If signature does not match Success(false) is returned
   // This is a valid function
   // because the same inputs will result in the same outputs.
   function method {:extern "Signature.ECDSA", "Verify"} Verify(