//= aws-encryption-sdk-specification/framework/structures.md#overview
//= type=exception
//# While these structures will usually be represented as objects, lower level languages MAY represent
//# these fields in a less strictly defined way as long as all field properties are still upheld.

//= aws-encryption-sdk-specification/framework/structures.md#structure
//= type=exception
//# This specification uses the terms "encrypt" and "decrypt" for simplicity,
//# but the actual process by which a key provider obtains the plaintext data key from the ciphertext
//# and vice versa MAY be any reversible operation, though we expect that most will use encryption.



This could only be asserted for ESDK provided keyrings.
But customers can roll their own.
//= aws-encryption-sdk-specification/framework/structures.md#ciphertext
//= type=exception
//# Some key provider MUST be capable of deterministically obtaining the plaintext key from the ciphertext.


These are requirements for users and documentation.
The "associated with the message" may be something
that could be proven at some point.
//= aws-encryption-sdk-specification/framework/structures.md#structure-1
//= type=exception
//# Users SHOULD use the encryption context to store:
//# 
//# - Non-secret data that MUST remain associated with the [message](../data-format/message.md) ciphertext.
//# - Data that is useful in logging and tracking, such as data about the file type, purpose, or ownership.
//# 
//# Users MUST NOT use the encryption context to store secret data.

This is a requirement placed on keyring developers.
//= aws-encryption-sdk-specification/framework/structures.md#encrypted-data-keys
//= type=exception
//# The [ciphertext](#ciphertext) of each encrypted data key in this list MUST be an opaque form of the
//# plaintext data key from this set of encryption materials.

This data is stored in Dafny,
but asserting this is true in the native runtimes does not seem tractable.
//= aws-encryption-sdk-specification/framework/structures.md#plaintext-data-key
//= type=exception
//# The plaintext data key SHOULD be stored as immutable data.

Dafny does not have any current way to ensure this.
//= aws-encryption-sdk-specification/framework/structures.md#plaintext-data-key
//= type=exception
//# The plaintext data key SHOULD offer an interface to zero the plaintext data key.

This is a requirement placed on CMM developers.
//= aws-encryption-sdk-specification/framework/structures.md#signing-key
//= type=exception
//# The value of this key MUST be kept secret.

This data is stored in Dafny,
but asserting this is true in the native runtimes does not seem tractable.
//= aws-encryption-sdk-specification/framework/structures.md#plaintext-data-key-1
//= type=exception
//# The plaintext data key SHOULD be stored as immutable data.

Dafny does not have any current way to ensure this.
//= aws-encryption-sdk-specification/framework/structures.md#plaintext-data-key-1
//= type=exception
//# The plaintext data key SHOULD offer an interface to zero the plaintext data key.