lawful-bytes

Releases (2)

• 0.1.1.0 indexed
• 0.1.0.0 unindexed

Definitions (578)

bytes.bend

• def emptyAn empty Bytes with room for 4 * 2^d bytes.
• def at.fin
• def atByte i (for i < len).
• def set.fin
• def setByte i set to v (for i < len and v < 256).
• def push.fin
• def pushv added at the end (for len < cap and v < 256).
• def append.gon more bytes of src, from s; r holds src's byte s.
• def appenddst with bytes s ..
• def grow.goWord i onwards copied into dst; r holds word i of the old block.

LAWS.bend

• law view_size
• law view_bytes
• law cap_ok
• law empty_view
• law empty_ok
• law grow_viewgrow keeps the bytes in a larger block.
• law grow_ok
• law at_view
• law at_pairThe result as a literal pair: the same Bytes and the value (for rewriting).
• law find_viewfind answers the first index in from ..
• law find_pairThe result as a literal pair: the same Bytes and the value (for rewriting).
• law find2_view
• law find2_pairThe result as a literal pair: the same Bytes and the value (for rewriting).
• law same_viewsame compares two ranges of equal length, n bytes each.
• law same_pairsame hands both buffers back (as a literal tuple, for rewriting).
• law set_view
• law set_ok
• law push_view
• law push_ok
• law append_viewappend adds n bytes of src, from s, at the end of dst.
• law append_ok
• law append_pairappend hands src back (as a literal pair, for rewriting).
• law len_view
• law len_pair
• law capacity_view
• law capacity_pair
• law truncate_view
• law truncate_ok
• law shift_viewshift drops the first k bytes and moves the rest to the start (for reusing a buffer when reading a stream in pieces).
• law shift_ok
• law of_list_view
• law of_list_ok
• law to_list_view
• law to_list_pair
• law same1_view
• law same1_pair
• law first_range
• law first_hitBelow to, the answer holds c.
• law first_missNo index from from up to the answer holds c.
• law first2_range
• law first2_hit
• law first2_miss
• law list_eq_trueA passed list_eq test gives equal lists.
• law list_eq_reflEqual lists pass list_eq.
• law fast_findThe word-at-a-time find gives exactly the reference result (the same Bytes and the same index).
• law fast_find2
• law fast_find_pairThe fast searches hand back the same Bytes, for any arguments (as find_pair and find2_pair say of the reference).
• law fast_find2_pair
• law fast_append_viewThe word-at-a-time append writes whole words, so up to 3 bytes past the new length differ from the reference's: its laws are append's, on the view.
• law fast_append_ok
• law fast_append_pair

PROOF.bend

• def at_view.go
• def view_size.go
• def view_bytes.go
• def cap_ok.go
• def grow_view.go
• def grow_ok.go
• def at_pair.go
• def find_view.go
• def find_pair.go
• def find2_view.go
• def find2_pair.go
• def same_view.go
• def same_pair.go
• def set_view.go
• def set_ok.go
• def push_view.go
• def push_ok.go
• def append_view.go
• def append_ok.go
• def append_pair.go
• def len_view.go
• def len_pair.go
• def capacity_view.go
• def capacity_pair.go
• def truncate_view.go
• def truncate_ok.go
• def shift_view.go
• def shift_ok.go
• def to_list_view.go
• def to_list_pair.go
• def same1_view.go
• def same1_pair.go
• def fast_find.go
• def fast_find2.go
• def fast_find_pair.go
• def fast_find2_pair.go
• def fast_append_view.go
• def fast_append_ok.go
• def fast_append_pair.go