qasim-bend-kit

Releases (2)

• 0.1.0.2 indexed
• 0.1.0.1 unindexed

Definitions (1,592)

libs/AES256GCM.bend

• def bytes_validAES-256-GCM with validated inputs and canonical envelope serialization.
• def core_bytes_valid_eq
• def core_bytes_valid_proof
• def length_pair_high
• def length_pair_within
• def bytes_length_limit.go
• def bytes_length_limit
• def plaintext_validGCM limits are expressed in bytes after requiring byte-aligned input.
• def aad_valid
• type SecretKey
• type Nonce
• type Tag
• type Envelope
• type Error
• law keyConstructors validate raw input; SecretKey/Nonce/Tag certificates enforce sizes.
• law nonce
• law encryptDeterministic primitive: the caller supplies a nonce unique for this key.
• law decryptFail contains only an Error, never unauthenticated or partial plaintext.
• law encodeCanonical envelope: v1.<lowercase nonce hex>.<lowercase tag hex>.<ciphertext hex>.
• law parse
• def nonce_bytesRead-only projections needed to state the contract.
• def tag_bytes
• def tag_bytes_size
• def tag_bytes_valid
• def ciphertext
• def envelope_ciphertext_valid
• def envelope_nonce
• def envelope_tag
• def hex_digit_kindCanonical lowercase hexadecimal envelope serialization.
• def hex_word_andThe mask-first implementation keeps zero mask bits visibly false to Bend's checker, which supports the nibble range proofs used by the codec.
• def hex_mask
• def hex_digit.nibble
• def hex_digit
• def hex_bytes
• def fixed_bytesSerialize validated fixed-size fields through a fixed-size byte view.
• def encode_impl
• def hex_nibbleMatch the ASCII code point directly so each accepted nibble normalizes to a literal.
• def hex_join
• def hex_pair.combine
• def hex_pair
• def hex_pairs
• def collect_hex.cons
• def collect_hex
• def decode_hex
• def aes_nat_eq_step
• def aes_nat_eq_proof
• def aes_bool_true_proof
• def aes_bytes_valid_cons_proof
• def aes_bytes_valid_from_bool
• def aes_bytes_valid_proof
• def key_checked
• def key_from_proofs
• def key_impl
• def nonce_checked
• def nonce_from_proofs
• def nonce_impl
• def secret_key_bytes
• def raw_nonce_bytes
• def tag_from_proofs
• def envelope_from_proofs
• def envelope_from_tag_proof

PROOF.bend

• def parallel_single
• def assemble_source
• def parse_number_payload
• def assembled_string_payload
• def parse_string_payload
• def parse_leading_space
• def parse_trailing_space
• def parse_trailing_tab
• def parse_trailing_return
• def parse_trailing_newline
• def parse_suffix_space
• def parse_suffix_tab
• def parse_suffix_return
• def parse_suffix_newline
• def parse_leading_surround
• def parse_surrounding_space
• def aes_nat_tail_ne
• def aes_nat_pred
• def aes_nat_zero_ne_succ
• def aes_nat_succ_ne_zero
• def aes_nat_eq_step_status
• def aes_nat_eq_refl_is_some
• def aes_nat_eq_is_some
• def aes_nat_eq_none_if_ne
• def aes_bytes_proof_none_if_invalid
• def aes_bytes_valid_none_if_false
• def aes_bytes_valid_status
• def aes_bytes_cert_is_some
• def aes_key_from_no_size
• def aes_key_from_no_valid
• def aes_nonce_from_no_size
• def aes_nonce_from_no_valid
• def encrypt_invalid_plaintext
• def encrypt_using_plaintext_validity
• def encrypt_invalid_aad
• def encrypt_using_aad_validity
• def decrypt_invalid_aad
• def decrypt_using_aad_validity
• def aes256gcm_nist_j0_block_checkpointKeep the composed NIST AES block certificate in the law proof book.