public static EncryptedDataKeyDescription EncryptedDataKeyDescription()

in DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java [444:494]


  public static EncryptedDataKeyDescription EncryptedDataKeyDescription(
    software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedDataKeyDescription nativeValue
  ) {
    DafnySequence<? extends Character> keyProviderId;
    keyProviderId =
      software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
        nativeValue.keyProviderId()
      );
    Option<DafnySequence<? extends Character>> keyProviderInfo;
    keyProviderInfo =
      Objects.nonNull(nativeValue.keyProviderInfo())
        ? Option.create_Some(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
          software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
            nativeValue.keyProviderInfo()
          )
        )
        : Option.create_None(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
        );
    Option<DafnySequence<? extends Character>> branchKeyId;
    branchKeyId =
      Objects.nonNull(nativeValue.branchKeyId())
        ? Option.create_Some(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
          software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
            nativeValue.branchKeyId()
          )
        )
        : Option.create_None(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
        );
    Option<DafnySequence<? extends Character>> branchKeyVersion;
    branchKeyVersion =
      Objects.nonNull(nativeValue.branchKeyVersion())
        ? Option.create_Some(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
          software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
            nativeValue.branchKeyVersion()
          )
        )
        : Option.create_None(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
        );
    return new EncryptedDataKeyDescription(
      keyProviderId,
      keyProviderInfo,
      branchKeyId,
      branchKeyVersion
    );
  }