// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0

include "../Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy"
  // Yes, this is reaching across.
  // idealy all these functions would exist in the STD Library.
include "../../TestVectorsAwsCryptographicMaterialProviders/src/JSONHelpers.dfy"

module {:options "-functionSyntax:4"} KeyDescription {
  import opened Wrappers
  import opened JSON.Values
  import AwsCryptographyMaterialProvidersTypes
  import opened Types = AwsCryptographyMaterialProvidersTestVectorKeysTypes
  import opened JSONHelpers
  import ComAmazonawsKmsTypes


  function printErr(e: string) : (){()} by method {print e, "\n", "\n"; return ();}
  function printJSON(e: seq<(string, JSON)>) : (){()} by method {print e, "\n", "\n"; return ();}

  function ToKeyDescription(obj: JSON): Result<KeyDescription, string>
  {
    :- Need(obj.Object?, "KeyDescription not an object");
    var obj := obj.obj;
    var typString := "type";
    var typ :- GetString(typString, obj);

    :- Need(KeyDescriptionString?(typ), "Unsupported KeyDescription type:" + typ);

    match typ
    case "aws-kms-mrk-aware-discovery" =>
      var defaultMrkRegion :- GetString("default-mrk-region", obj);
      var filter := GetObject("aws-kms-discovery-filter", obj);
      var awsKmsDiscoveryFilter := ToDiscoveryFilter(obj);
      Success(KmsMrkDiscovery(KmsMrkAwareDiscovery(
                                keyId := "aws-kms-mrk-aware-discovery",
                                defaultMrkRegion := defaultMrkRegion,
                                awsKmsDiscoveryFilter := awsKmsDiscoveryFilter
                              )))
    case _ =>
      var key :- GetString("key", obj);
      match typ
      case "static-material-keyring" =>
        Success(Static(StaticKeyring( keyId := key )))
      case "aws-kms" =>
        Success(Kms(KMSInfo( keyId := key )))
      case "aws-kms-mrk-aware" =>
        Success(KmsMrk(KmsMrkAware( keyId := key )))
      case "aws-kms-rsa" =>
        var encryptionAlgorithmString :- GetString("encryption-algorithm", obj);
        :- Need(EncryptionAlgorithmSpec?(encryptionAlgorithmString), "Unsupported EncryptionAlgorithmSpec:" + encryptionAlgorithmString);
        var encryptionAlgorithm := match encryptionAlgorithmString
          case "RSAES_OAEP_SHA_1" => ComAmazonawsKmsTypes.EncryptionAlgorithmSpec.RSAES_OAEP_SHA_1
          case "RSAES_OAEP_SHA_256" => ComAmazonawsKmsTypes.EncryptionAlgorithmSpec.RSAES_OAEP_SHA_256;
        Success(KmsRsa(KmsRsaKeyring( keyId := key, encryptionAlgorithm := encryptionAlgorithm )))
      case "aws-kms-hierarchy" =>
        Success(Hierarchy(HierarchyKeyring( keyId := key )))
      case "raw" =>
        var algorithm :- GetString("encryption-algorithm", obj);
        var providerId :- GetString("provider-id", obj);
        :- Need(RawAlgorithmString?(algorithm), "Unsupported algorithm:" + algorithm);
        match algorithm
        case "aes" =>
          Success(AES(RawAES( keyId := key, providerId := providerId )))
        case "rsa" =>
          var paddingAlgorithm :- GetString("padding-algorithm", obj);
          var paddingHash :- GetString("padding-hash", obj);
          :- Need(PaddingAlgorithmString?(paddingAlgorithm), "Unsupported paddingAlgorithm:" + paddingAlgorithm);
          :- Need(PaddingHashString?(paddingHash), "Unsupported paddingHash:" + paddingHash);

          match paddingAlgorithm
          case "pkcs1" =>
            :- Need(paddingHash == "sha1", "Unsupported padding with pkcs1:" + paddingHash);
            Success(RSA(RawRSA( keyId := key, providerId := providerId, padding := AwsCryptographyMaterialProvidersTypes.PKCS1 )))
          case "oaep-mgf1" => match paddingHash
            case "sha1" => Success(RSA(RawRSA( keyId := key, providerId := providerId, padding := AwsCryptographyMaterialProvidersTypes.OAEP_SHA1_MGF1 )))
            case "sha256" => Success(RSA(RawRSA( keyId := key, providerId := providerId, padding := AwsCryptographyMaterialProvidersTypes.OAEP_SHA256_MGF1 )))
            case "sha384" => Success(RSA(RawRSA( keyId := key, providerId := providerId, padding := AwsCryptographyMaterialProvidersTypes.OAEP_SHA384_MGF1 )))
            case "sha512" => Success(RSA(RawRSA( keyId := key, providerId := providerId, padding := AwsCryptographyMaterialProvidersTypes.OAEP_SHA512_MGF1 )))
  }

  function ToDiscoveryFilter(obj: seq<(string, JSON)>)
    : Option<AwsCryptographyMaterialProvidersTypes.DiscoveryFilter>
  {
    var filter :- GetObject("aws-kms-discovery-filter", obj).ToOption();
    var partition :- GetString("partition", filter).ToOption();
    var accountIds :- GetArrayString("account-ids", filter).ToOption();
    Some(AwsCryptographyMaterialProvidersTypes.DiscoveryFilter(
           partition := partition,
           accountIds := accountIds
         ))
  }

  predicate KeyDescriptionString?(s: string)
  {
    || s == "static-material-keyring"
    || s == "aws-kms"
    || s == "aws-kms-mrk-aware"
    || s == "aws-kms-mrk-aware-discovery"
    || s == "raw"
    || s == "aws-kms-hierarchy"
    || s == "aws-kms-rsa"
  }

  predicate RawAlgorithmString?(s: string)
  {
    || s == "aes"
    || s == "rsa"
  }

  predicate PaddingAlgorithmString?(s: string)
  {
    || s == "pkcs1"
    || s == "oaep-mgf1"
  }

  predicate PaddingHashString?(s: string)
  {
    || s == "sha1"
    || s == "sha1"
    || s == "sha256"
    || s == "sha384"
    || s == "sha512"
  }

  predicate EncryptionAlgorithmSpec?(s: string)
  {
    // This is missing SYMMETRIC_DEFAULT because this is asymmetric only
    || s == "RSAES_OAEP_SHA_1"
    || s == "RSAES_OAEP_SHA_256"
  }

}