DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java [335:402]:
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
    Option<
      DafnySequence<? extends DafnySequence<? extends Character>>
    > allowedUnsignedAttributes;
    allowedUnsignedAttributes =
      (Objects.nonNull(nativeValue.allowedUnsignedAttributes()) &&
          nativeValue.allowedUnsignedAttributes().size() > 0)
        ? Option.create_Some(
          DafnySequence._typeDescriptor(
            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
          ),
          software.amazon.cryptography.services.dynamodb.internaldafny.ToDafny.AttributeNameList(
            nativeValue.allowedUnsignedAttributes()
          )
        )
        : Option.create_None(
          DafnySequence._typeDescriptor(
            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
          )
        );
    Option<DafnySequence<? extends Character>> allowedUnsignedAttributePrefix;
    allowedUnsignedAttributePrefix =
      Objects.nonNull(nativeValue.allowedUnsignedAttributePrefix())
        ? Option.create_Some(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
          software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
            nativeValue.allowedUnsignedAttributePrefix()
          )
        )
        : Option.create_None(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
        );
    Option<DBEAlgorithmSuiteId> algorithmSuiteId;
    algorithmSuiteId =
      Objects.nonNull(nativeValue.algorithmSuiteId())
        ? Option.create_Some(
          DBEAlgorithmSuiteId._typeDescriptor(),
          software.amazon.cryptography.materialproviders.ToDafny.DBEAlgorithmSuiteId(
            nativeValue.algorithmSuiteId()
          )
        )
        : Option.create_None(DBEAlgorithmSuiteId._typeDescriptor());
    Option<IKeyring> keyring;
    keyring =
      Objects.nonNull(nativeValue.keyring())
        ? Option.create_Some(
          TypeDescriptor.reference(IKeyring.class),
          software.amazon.cryptography.materialproviders.ToDafny.Keyring(
            nativeValue.keyring()
          )
        )
        : Option.create_None(TypeDescriptor.reference(IKeyring.class));
    Option<ICryptographicMaterialsManager> cmm;
    cmm =
      Objects.nonNull(nativeValue.cmm())
        ? Option.create_Some(
          TypeDescriptor.reference(ICryptographicMaterialsManager.class),
          software.amazon.cryptography.materialproviders.ToDafny.CryptographicMaterialsManager(
            nativeValue.cmm()
          )
        )
        : Option.create_None(
          TypeDescriptor.reference(ICryptographicMaterialsManager.class)
        );
    Option<LegacyOverride> legacyOverride;
    legacyOverride =
      Objects.nonNull(nativeValue.legacyOverride())
        ? Option.create_Some(
          LegacyOverride._typeDescriptor(),
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -



DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToDafny.java [148:215]:
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
    Option<
      DafnySequence<? extends DafnySequence<? extends Character>>
    > allowedUnsignedAttributes;
    allowedUnsignedAttributes =
      (Objects.nonNull(nativeValue.allowedUnsignedAttributes()) &&
          nativeValue.allowedUnsignedAttributes().size() > 0)
        ? Option.create_Some(
          DafnySequence._typeDescriptor(
            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
          ),
          software.amazon.cryptography.services.dynamodb.internaldafny.ToDafny.AttributeNameList(
            nativeValue.allowedUnsignedAttributes()
          )
        )
        : Option.create_None(
          DafnySequence._typeDescriptor(
            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
          )
        );
    Option<DafnySequence<? extends Character>> allowedUnsignedAttributePrefix;
    allowedUnsignedAttributePrefix =
      Objects.nonNull(nativeValue.allowedUnsignedAttributePrefix())
        ? Option.create_Some(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
          software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
            nativeValue.allowedUnsignedAttributePrefix()
          )
        )
        : Option.create_None(
          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
        );
    Option<DBEAlgorithmSuiteId> algorithmSuiteId;
    algorithmSuiteId =
      Objects.nonNull(nativeValue.algorithmSuiteId())
        ? Option.create_Some(
          DBEAlgorithmSuiteId._typeDescriptor(),
          software.amazon.cryptography.materialproviders.ToDafny.DBEAlgorithmSuiteId(
            nativeValue.algorithmSuiteId()
          )
        )
        : Option.create_None(DBEAlgorithmSuiteId._typeDescriptor());
    Option<IKeyring> keyring;
    keyring =
      Objects.nonNull(nativeValue.keyring())
        ? Option.create_Some(
          TypeDescriptor.reference(IKeyring.class),
          software.amazon.cryptography.materialproviders.ToDafny.Keyring(
            nativeValue.keyring()
          )
        )
        : Option.create_None(TypeDescriptor.reference(IKeyring.class));
    Option<ICryptographicMaterialsManager> cmm;
    cmm =
      Objects.nonNull(nativeValue.cmm())
        ? Option.create_Some(
          TypeDescriptor.reference(ICryptographicMaterialsManager.class),
          software.amazon.cryptography.materialproviders.ToDafny.CryptographicMaterialsManager(
            nativeValue.cmm()
          )
        )
        : Option.create_None(
          TypeDescriptor.reference(ICryptographicMaterialsManager.class)
        );
    Option<LegacyOverride> legacyOverride;
    legacyOverride =
      Objects.nonNull(nativeValue.legacyOverride())
        ? Option.create_Some(
          LegacyOverride._typeDescriptor(),
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -