lawful-bytes

Releases (2)

• 0.1.1.0 indexed
• 0.1.0.0 unindexed

Definitions (578)

proof_ops.bend

• law push_eq_t
• law push_roomThe room test of push, as numbers.
• law push_view_t
• law push_ok_t
• law capacity_pair_t
• law capacity_view_t
• law truncate_view_t
• law truncate_ok_t

proof_same.bend

• def mdisc
• law none_some
• law drop_zero
• law drop_getDropping j elements, when element j is x: x, then the rest.
• law slice_cons
• law lt_of_lea + 1 + m <= b gives a < b.
• law le_stepa + 1 + m <= b gives (a + 1) + m <= b.
• law step_valOne step of a read loop at index s with n + 1 left, within a Bytes of size len: byte s is read, s + 1 does not wrap, and the bound holds one index on.
• law step_inc
• law step_le
• law tl_pair
• law append_nil
• law get_drop
• law take_snocTaking k + 1 elements then acc is taking k then element k, then acc.
• law slice_snoc
• law tl_valByte j, for j = m + s below len, is element m + s of the view.
• law tl_decj - 1 for j = 1 + m + s.
• law tl_lt
• law tl_view
• law tl_view_kto_list(BT, s, n) with k = n bytes: none, or 1 + p read from s + n - 1.
• law to_list_pair_t
• law to_list_view_t
• law and_assoc
• law lists_endComparing n more bytes from i of A and from j of B, after an empty prefix: acc and the comparison of the two slices.
• law lists_stepOne step of a comparison loop: the two slices from x and y, with the accumulated test rebracketed.
• law sm_pair
• law sm_view
• law same_pair_t
• law same_view_t
• law at2_eq
• law s1_pair
• law s1_view
• law same1_pair_t
• law same1_view_t

proof_seq.bend

• law take_zero
• law take_length
• law take_take
• law take_set
• law take_set_succSetting index n and keeping n + 1 elements: the first n, then v.
• law take_append_l
• law unpack_length4
• law unpack_length
• law unpack_append
• law all_bytes_unpack
• law all_bytes_take

proof_shift.bend

• law get_drop
• law drop_length
• law drop_set0Setting the first element of drop(xs, j).
• law take_snoc
• law take_all
• law sub_self
• def SGT
• law shift_go_eq
• law sgt_ok
• def SVBytes j onwards are still those of xs; bytes below j are xs from k on.
• law sv_ltNat facts for one step: j + k + (1 + n) = L.
• law sv_lt_j
• law sv_m
• law sv_jk1
• def SFThe final view: SV at j = L - k.
• law sv_readThe value read at p = j + k is element j of drop(xs, k).
• law sv_writeWriting that value at j moves the boundary to j + 1.
• law sub_le
• law xldrop(xs, k) has L - k elements.
• law sv_jdj <= L - k from j + k < L.
• law sv_xThe byte read at p is element j of drop(xs, k).
• law sv
• law sv0
• law shift_view_t
• law shift_ok_t