bend-osdev-bytes
Releases (3)
Definitions (396)
LAWS.bend
- law octets_le32_at_append_add
- law octets_le32_at_append_le
- law octets_le32_at_drop
- law octets_le32_at_take
- law octets_be32_at_append_add
- law octets_be32_at_append_le
- law octets_be32_at_drop
- law octets_be32_at_take
- law octets_le64_at_append_add
- law octets_le64_at_append_le
- law octets_le64_at_drop
- law octets_le64_at_take
- law octets_be64_at_append_add
- law octets_be64_at_append_le
- law octets_be64_at_drop
- law octets_be64_at_take
- law low16_mask
PROOF.bend
- def le32_head_appReading a 32-bit field at the head of a longer string, and skipping it
- def be32_head_app
- def drop4_le32
- def drop4_be32
- def field64_lethe eight bytes of two le32 fields come back unchanged through Octets
- def field64_bethe eight bytes of two be32 fields come back unchanged through Octets
- def bits8_of_bits8
- def w8s_of_to
- def oct_bytea word through one OctByte and back is its byte
- def w8s_to_of
- def w8s_to_app
- def w8s_len
- def w8s_take_drop
- def w8s_take_app
- def w8s_drop_app
- def w8s_len_app
- def r8_rr
- def ru_rr
- def app_nil8
- def app_nilu
- def g_of
- def F_of
- def g_to
- def F_to
- def g_take
- def F_take
- def F_app
- def g_len
- def F_len
- def zeros_cons
- def g_zeros
- def F_zeros
- def w8s_zeros_list
- def p_octets_take_drop
- def p_octets_of_to
- def p_octets_to_of
- def u32_eq_self
- def list_eq_self
- def w8s_eq_self
- def p_octets_append_list
- def p_octets_len_list
- def p_octets_take_append
- def p_octets_drop_append
- def p_octets_split_at_append
- def p_octets_zeros_list
- def p_octets_cons_list
- def ru_app_nil
- def g_lenu
- def p_len_fast
- def rr_backa structural list, reversed onto Nil and back, is itself
- def g_takeu
- def p_take_fast
- def p_append_fast
- def zeros_consu
- def g_zerosu
- def p_zeros_fast
- def g_mask
- def p_mask_fast
- def g_of_string
- def p_of_string_fast
- def t_gotext: building from the back onto acc is the structural cat
- def t_cat
- def p_to_string_fast
- def h_go
- def h_cat
- def p_hex_fast
- def eq_go
- def p_list_eq_fast
- def w_t_goOctets' text and hex: each word read through bits8/of_bits8 is its byte
- def p_octets_to_string_list
- def w_h_go
- def p_octets_hex_list
- def rev_app8concat: pushing each piece's words is reversing the joined words
- def concat_step
- def concat_go
- def octets_eta
- def rr8_back
- def concat_ref
- def p_octets_concat_cons
- def off.disc
- def off.clash
- def off.absurd
- def off.no