bend-osdev-mode-core

Releases (1)

• 0.1.0.0 indexed

Definitions (151)

check.bend

• def toy.rotA toy permutation of blocks, NOT a cipher: the words rotated, then XOR with the key block.
• def toy.unrot
• def toy.enc
• def toy.dec
• def key
• def key2
• def hexs
• def maybe
• def main

LAWS.bend

• law block_octets_round_tripA block written as Octets reads back as the same block, for every block
• law byte_byte
• law split_cons_blocks
• law split_cons_tail
• law split_eta
• law list_take_append
• law list_drop_append
• law list_mask_append
• law list_mask_take
• law list_len_append
• law list_len_take
• law nat_lt_le
• law split_bytes_ontosplitting the bytes of a block gives the block back
• law mask_bytes_ontothe bytes of a block are bytes: masking changes nothing
• law join_splita masked list is its blocks and its tail joined back
• law bytes_onto_block16the bytes of the block of any 16 values are those values, masked
• law split_tail_shortthe tail of a split has fewer than 16 bytes
• law split_tail_maskedthe tail of a masked split is masked
• law split_shortfewer than 16 bytes are all tail
• law block_of_bytes_ofthe block of a block's bytes is the block
• law octets_maskedEvery Octets is masked: to_list(o) = to_list(of_list(to_list(o))) = mask(to_list(o))
• law octets_len
• law blocks_len_fast
• law split_fast
• law join_onto_fast
• law bind_conga bind whose continuations agree on every value agrees
• law dec_enc_headthe first block's round trip, and the rest's
• law dec_enc_tail
• law word_xor_xor
• law u32_xor_xor
• law block_xor_xor
• law mask_join_onto
• law split_join_shortblocks joined in front of a short tail split back into those blocks and tail

PROOF.bend

• def bits.word_bytes
• def bits.byte0_word
• def bits.byte1_word
• def bits.byte2_word
• def bits.byte3_word
• def bits.byte_b0
• def bits.byte_b1
• def bits.byte_b2
• def bits.byte_b3
• def bits.byte_byte
• def sp.cons_blocks
• def sp.cons_tail
• def sp.eta
• def bo.disc
• def bo.empty
• def bo.absurd
• def li.mask_mask
• def li.take_append
• def li.drop_append
• def li.mask_append
• def li.mask_take
• def li.len_append
• def li.len_take
• def na.lt_le
• def sp.blksplitting the bytes of a block gives the block back
• def sp.mask_blkthe bytes of a block are bytes: masking changes nothing
• def sp.blk16the block of 16 bytes, as bytes again
• def sp.join_splita masked list is its blocks and its tail joined back
• def sp.blk16gthe bytes of the block of any 16 values are those values, masked
• def sp.tail_shortthe tail of a split has fewer than 16 bytes
• def sp.tail_maskedthe tail of a masked split is masked
• def sp.short_splitfewer than 16 bytes are all tail
• def sp.block_bytesthe block of a block's bytes is the block
• def oc.maskedEvery Octets is masked: to_list(o) = to_list(of_list(to_list(o))) = mask(to_list(o))
• def oc.len
• def tr.len_go
• def tr.len_eq
• def tr.split_fin
• def tr.split_fin_cons
• def tr.split_fin_nil
• def tr.split_go
• def tr.split_eq
• def tr.join_go
• def tr.join_eq
• def tr.bind_conga bind whose continuations agree on every value agrees
• def cmp.head
• def cmp.tail
• def li.con_hd
• def li.con_tl
• def cmp.hdthe first block's round trip, and the rest's
• def cmp.tl
• def bx.rbool
• def bx.rword
• def bx.ru32
• def bx.rblock
• def sp.mask_join_onto
• def sp.split_join_shortblocks joined in front of a short tail split back into those blocks and tail
• def li.len_bytes