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_NistVectorProof.bend

• def partial_block_tag
• def partial_block_auth
• def checkpoint_partial_block_plaintext_stream
• def checkpoint_partial_block_ciphertext_stream
• def checkpoint_partial_block_ciphertext
• def checkpoint_partial_block_ghash
• def checkpoint_partial_block_tag
• def partial_block_encrypt
• def checkpoint_partial_block_plaintext
• def checkpoint_partial_block_authenticated
• def partial_block_decrypt

proof/AES_StringEqProof.bend

• def false_type
• def false_true
• def cmp_eq_of_true
• def tag_is_snd
• def string_eq_sound
• def string_eq_self

proof/AES_TagCompareProof.bend

• def diff_same
• def equal_same
• def equal_of_equal
• def diff_acc_zero
• def diff_list_sound
• def equal_sound
• def unequal_from_bool
• def unequal_is_false

proof/AES_TagRejectProof.bend

• def rejects_comparison
• def rejects_tag

proof/AES_TamperProof.bend

• def canonical_for_equal_envelope
• def reject_authenticated
• def rejects_changed_tag

proof/AES_TraceBridgeProof.bend

• def expand_input_matchesSubstitute a certified initial word list with a symbolic fuel parameter.
• def expand_key_matches
• def expansion_alias
• def public_expansion_matches

proof/AES_TraceProof.bend

• def next_word
• def expand_step
• def rounds_step
• def expand_step_at
• def expand_step_number_at
• def rounds_fuel_matches
• def rounds_step_at

proof/AES_ZipLengthProof.bend

• def false_type
• def false_true
• def predecessor
• def zip_length_equal
• def encrypt_block_length
• def nat_add_succ_right
• def nat_add_zero_right
• def nat_add_comm
• def reverse_go_length
• def reverse_length
• def append_length
• def stream_step_length
• def ctr_stream_exact_go_length
• def ctr_stream_exact_length
• def ctr_encrypt_ciphertext_length

proof/JSON_AssemblyProof.bend

• def R
• type Mode
• def tokens
• def start_members
• def start
• def completed_members
• def completed
• def atom_roundtrip
• def array_first_atom
• def array_next_atom
• def array_first
• def array_next
• def roundtrip

proof/JSON_LexWhitespaceProof.bend

• def after_mode
• def after_reversed
• def after_acc
• def lexemes_step
• def lex_scan_step
• def prefix_mode
• def prefix_reversed
• def prefix_acc
• def prefix_mode_append
• def prefix_reversed_append
• def prefix_acc_append
• def lex_scan_append
• def lex_scan_context
• def scan_punctuation_char
• def raw_string_seed
• def scan_raw_string_char
• def scan_escape_char
• def escape_reverse
• def escape_reverse_shape
• def scan_escape_string
• def quoted_buffer_payload
• def lex_rendered_string
• def lex_rendered_string_suffix
• def lex_string_before_punctuation
• def lex_null_before_punctuation
• def lex_true_before_punctuation
• def lex_false_before_punctuation
• def lex_empty_array_before_punctuation
• def lex_empty_object_before_punctuation
• def trailing_space
• def trailing_tab