qasim-bend-kit

Releases (3)

• 0.1.0.2 indexed
• 0.1.0.1 unindexed
• 0.1.0.0 unindexed

Definitions (1,592)

proof/AES_CertificateProof.bend

• def nat_unique

proof/AES_ConstructorProof.bend

• def key_certificates
• def key_accepts
• def nonce_certificates
• def nonce_accepts
• def nonce_equal

proof/AES_CoreTagProof.bend

• def output_ciphertext
• def output_tag
• def output_tag_words
• def output_tag_nonce
• def output_tag_aad
• def output_tag_ciphertext
• def output_from_ciphertext_matches
• def output_ciphertext_valid
• def output_tag_valid
• def envelope_gcm_ciphertext
• def envelope_gcm_tag
• def envelope_gcm_nonce
• def raw_encrypt_output_ciphertext

proof/AES_EncryptProof.bend

• type TagContext
• def result_ciphertext
• def output_tag_context
• def tag_for_context
• def output_tag_matches_context
• def raw_output_tag_canonical
• def result_tag_bytes
• def valid_output_ciphertext_length
• def encrypt_checked_with_flags
• def successful_encrypt_aad_valid
• def successful_encrypt_plaintext_valid
• def result_ciphertext_length
• def successful_encrypt_preserves_length
• def successful_encrypt_ciphertext_matches_gcm
• def successful_encrypt_tag_matches_gcm
• def successful_encrypt_tag_canonical
• def successful_encrypt_ciphertext_matches_ctr
• def successful_encrypt_ciphertext_valid
• def successful_encrypt_ctr_decrypts
• def result_nonce
• def output_nonce
• def valid_nonce
• def checked_nonce
• def encrypt_nonce
• def preserves_nonce
• def successful_encrypt_envelope_tag_canonical
• def decrypt_auth_tag_canonical
• def successful_encrypt_decrypt_authenticated
• def successful_encrypt_decrypt_roundtrip
• def output_is_done
• def valid_is_done
• def valid_input_is_done

proof/AES_EnvelopeProof.bend

• def aes_hex_mask_15_lt_16
• def aes_hex_mask_255_lt_256
• def aes_bool_and_false
• def aes_bool_and_true
• def aes_hex_word_and_equiv
• def aes_hex_word_and_idempotent
• def aes_hex_mask_idempotent
• def aes_hex_digit_inverse
• def aes_hex_digit_no_dot
• def aes_split_hex_digit_no_dot
• def aes_hex_join_shift_mask
• def aes_hex_join_masked_shift_mask
• def aes_hex_byte_prefix_idempotent
• def aes_hex_mask_bytes
• def aes_hex_bytes_mask_idempotent
• def aes_hex_pair_roundtrip
• def aes_decode_hex_bytes
• def aes_split_push_single
• def aes_hex_bytes_split_single
• def aes_split_push_cons
• def aes_hex_bytes_split_before_period
• def aes_split_leading_dot
• def aes_split_v1_prefix
• def aes_string_append_assoc
• def aes_split_v1_hex_fields
• def aes_encode_fields_split
• def aes_false_type
• def aes_false_true
• def aes_nat_predecessor
• def aes_fixed_bytes_length
• def aes_fixed_bytes_identity
• def aes_parse_decoded_masked_map
• def aes_hex_mask_bytes_length
• def aes_hex_mask_bytes_valid
• def aes_nat_eq_self
• def aes_bytes_valid_status
• def aes_masked_bytes_cert_is_some
• def aes_nat_eq_is_some
• def aes_masked_size_is_some
• def aes_maybe_cert_value
• def aes_maybe_cert_reconstruct
• def aes_parse_decoded_map_goal
• def aes_parse_decoded_if_some
• def aes_parse_decoded_checked_map
• def aes_parse_decoded_hex_map
• def aes_parse_fields_hex_map
• def aes_parse_encoder_fields_map
• def aes_parse_fields_encoded_map
• def aes_envelope_roundtrip