bend-osdev-bytes Releases (3): 0.1.1.1 0x15cc157649e26d54c7c549cb80d4a2a9 invalid https://jend.leeeet.dev/files.txt?path=bend-osdev-bytes@0.1.1.1 expected a package named bend-osdev-word64@0.1.1.1 on https://hub.bend-lang.com At https://jend.leeeet.dev/read.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&start_line=5, https://jend.leeeet.dev/read.txt?path=bend-osdev-bytes@0.1.1.1/PROOF.bend&start_line=2, https://jend.leeeet.dev/read.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&start_line=12, https://jend.leeeet.dev/read.txt?path=bend-osdev-bytes@0.1.1.1/check.bend&start_line=2. Files that do not load: LAWS.bend, PROOF.bend, bytes.bend, check.bend, package.bend. 0.1.1.0 0xe0217e1ab38629fddf738452c1f2a82e indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-bytes@0.1.1.0 0.1.0.0 0x9df7f91779a4a1c215bfa96cd0864601 unindexed https://jend.leeeet.dev/files.txt?path=bend-osdev-bytes@0.1.0.0 Definitions (396, 1 to 100 shown): LAWS.le16_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=le16_round_trip) law le16_round_trip: for v: U32 {B.le16_at(B.le16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>} LAWS.be16_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=be16_round_trip) law be16_round_trip: for v: U32 {B.be16_at(B.be16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>} LAWS.le32_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=le32_round_trip) law le32_round_trip: for v: U32 {B.le32_at(B.le32(v), 0n) == Some{v} : Maybe<&2, U32>} LAWS.be32_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=be32_round_trip) law be32_round_trip: for v: U32 {B.be32_at(B.be32(v), 0n) == Some{v} : Maybe<&2, U32>} LAWS.le64_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=le64_round_trip) law le64_round_trip: for +v: W.W64 {B.le64_at(B.le64(v), 0n) == Some{v} : Maybe<&2, W.W64>} LAWS.be64_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=be64_round_trip) law be64_round_trip: for +v: W.W64 {B.be64_at(B.be64(v), 0n) == Some{v} : Maybe<&2, W.W64>} LAWS.byte_below_256 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=byte_below_256) law byte_below_256: for b: U32 {U32.is_lt(B.byte(b), 256) == True{} : Bool} LAWS.take_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=take_drop) law take_drop: for n: Nat for xs: List<&2, U32> {B.append(B.take(n, xs), B.drop(n, xs)) == xs : List<&2, U32>} LAWS.be32_order (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=be32_order) law be32_order: {B.be32(305419896) == [18, 52, 86, 120] : List<&2, U32>} LAWS.le32_order (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=le32_order) law le32_order: {B.le32(305419896) == [120, 86, 52, 18] : List<&2, U32>} LAWS.be64_order (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=be64_order) law be64_order: {B.be64(W.W64.from_parts(16909060, 84281096)) == [1, 2, 3, 4, 5, 6, 7, 8] : List<&2, U32>} LAWS.le16_at_offset (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=le16_at_offset) law le16_at_offset: {B.le16_at([9, 52, 18], 1n) == Some{4660} : Maybe<&2, U32>} LAWS.short_input (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=short_input) law short_input: {B.le16_at([1, 2, 3], 2n) == None{} : Maybe<&2, U32>} LAWS.at_end (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=at_end) law at_end: {B.at([7, 8], 2n) == None{} : Maybe<&2, U32>} LAWS.masks_elements (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=masks_elements) law masks_elements: {B.at([7, 264], 1n) == Some{8} : Maybe<&2, U32>} LAWS.hex_text (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=hex_text) law hex_text: {B.hex(B.of_string("Bend")) == "42656e64" : String} LAWS.octets_le16_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le16_round_trip) law octets_le16_round_trip: for v: U32 {B.Octets.le16_at(B.Octets.le16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>} LAWS.octets_be16_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_be16_round_trip) law octets_be16_round_trip: for v: U32 {B.Octets.be16_at(B.Octets.be16(v), 0n) == Some{B.low16(v)} : Maybe<&2, U32>} LAWS.octets_le32_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le32_round_trip) law octets_le32_round_trip: for v: U32 {B.Octets.le32_at(B.Octets.le32(v), 0n) == Some{v} : Maybe<&2, U32>} LAWS.octets_be32_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_be32_round_trip) law octets_be32_round_trip: for v: U32 {B.Octets.be32_at(B.Octets.be32(v), 0n) == Some{v} : Maybe<&2, U32>} LAWS.octets_le64_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le64_round_trip) law octets_le64_round_trip: for +v: W.W64 {B.Octets.le64_at(B.Octets.le64(v), 0n) == Some{v} : Maybe<&2, W.W64>} LAWS.octets_be64_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_be64_round_trip) law octets_be64_round_trip: for +v: W.W64 {B.Octets.be64_at(B.Octets.be64(v), 0n) == Some{v} : Maybe<&2, W.W64>} LAWS.octets_take_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_take_drop) law octets_take_drop: for n: Nat for o: B.Octets {B.Octets.append(B.Octets.take(n, o), B.Octets.drop(n, o)) == o : B.Octets} LAWS.octets_of_list_idempotent (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_of_list_idempotent) # of_list masks once: converting a byte string to a list and back changes nothing law octets_of_list_idempotent: for xs: List<&2, U32> {B.Octets.of_list(B.Octets.to_list(B.Octets.of_list(xs))) == B.Octets.of_list(xs) : B.Octets} LAWS.octets_is_eq_refl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_is_eq_refl) law octets_is_eq_refl: for o: B.Octets {B.Octets.is_eq(o, o) == True{} : Bool} LAWS.octets_masks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_masks) law octets_masks: {B.Octets.hex(B.Octets.of_list([255, 256, 257])) == "ff0001" : String} LAWS.octets_slice (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_slice) law octets_slice: {B.Octets.to_string(B.Octets.slice(2n, 3n, B.Octets.of_string("bend-osdev"))) == "nd-" : String} LAWS.octets_append_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_append_list) law octets_append_list: for a: B.Octets for b: B.Octets {B.Octets.to_list(B.Octets.append(a, b)) == B.append(B.Octets.to_list(a), B.Octets.to_list(b)) : List<&2, U32>} LAWS.octets_of_to (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_of_to) # every Octets is a valid byte string: to a list and back changes nothing law octets_of_to: for o: B.Octets {B.Octets.of_list(B.Octets.to_list(o)) == o : B.Octets} LAWS.octets_to_of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_to_of) # a list becomes Octets by masking each element to its low 8 bits law octets_to_of: for xs: List<&2, U32> {B.Octets.to_list(B.Octets.of_list(xs)) == B.mask(xs) : List<&2, U32>} LAWS.octets_zeros_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_zeros_list) law octets_zeros_list: for n: Nat {B.Octets.to_list(B.Octets.zeros(n)) == B.zeros(n) : List<&2, U32>} LAWS.octets_cons_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_cons_list) law octets_cons_list: for b: U32 for o: B.Octets {B.Octets.to_list(B.Octets.cons(b, o)) == Con{B.byte(b), B.Octets.to_list(o)} : List<&2, U32>} LAWS.octets_len_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_list) law octets_len_list: for o: B.Octets {B.Octets.len(o) == B.len(B.Octets.to_list(o)) : Nat} LAWS.octets_take_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_take_append) # a joined string splits back exactly where it was joined law octets_take_append: for +a: B.Octets for b: B.Octets {B.Octets.take(B.Octets.len(a), B.Octets.append(a, b)) == a : B.Octets} LAWS.octets_drop_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_drop_append) law octets_drop_append: for a: B.Octets for +b: B.Octets {B.Octets.drop(B.Octets.len(a), B.Octets.append(a, b)) == b : B.Octets} LAWS.octets_split_at_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_split_at_append) law octets_split_at_append: for +a: B.Octets for +b: B.Octets {B.Octets.split_at(B.Octets.len(a), B.Octets.append(a, b)) == Some{B.OctetsSplit{a, b}} : Maybe<&2, B.OctetsSplit>} LAWS.octets_split_short (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_split_short) law octets_split_short: {B.Octets.split_at(4n, B.Octets.of_string("abc")) == None{} : Maybe<&2, B.OctetsSplit>} LAWS.octets_split_text (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_split_text) law octets_split_text: {B.Octets.split_at(2n, B.Octets.of_string("abc")) == Some{B.OctetsSplit{B.Octets.of_string("ab"), B.Octets.of_string("c")}} : Maybe<&2, B.OctetsSplit>} LAWS.len_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=len_fast) law len_fast: for xs: List<&2, U32> {B.len(xs) == B.len.fast(xs) : Nat} LAWS.take_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=take_fast) law take_fast: for n: Nat for xs: List<&2, U32> {B.take(n, xs) == B.take.fast(n, xs) : List<&2, U32>} LAWS.append_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=append_fast) law append_fast: for xs: List<&2, U32> for ys: List<&2, U32> {B.append(xs, ys) == B.append.fast(xs, ys) : List<&2, U32>} LAWS.zeros_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=zeros_fast) law zeros_fast: for n: Nat {B.zeros(n) == B.zeros.fast(n) : List<&2, U32>} LAWS.mask_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=mask_fast) law mask_fast: for xs: List<&2, U32> {B.mask(xs) == B.mask.fast(xs) : List<&2, U32>} LAWS.of_string_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=of_string_fast) law of_string_fast: for s: String {B.of_string(s) == B.of_string.fast(s) : List<&2, U32>} LAWS.to_string_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=to_string_fast) law to_string_fast: for xs: List<&2, U32> {B.to_string(xs) == B.to_string.fast(xs) : String} LAWS.hex_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=hex_fast) law hex_fast: for xs: List<&2, U32> {B.hex(xs) == B.hex.fast(xs) : String} LAWS.list_eq_fast (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=list_eq_fast) law list_eq_fast: for xs: List<&2, U32> for ys: List<&2, U32> {B.list_eq(xs, ys) == B.list_eq.fast(xs, ys) : Bool} LAWS.rev_rev (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=rev_rev) law rev_rev: for xs: List<&2, U32> {B.rev(B.rev(xs)) == xs : List<&2, U32>} LAWS.octets_hex_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_hex_list) law octets_hex_list: for o: B.Octets {B.Octets.hex(o) == B.hex(B.Octets.to_list(o)) : String} LAWS.octets_to_string_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_to_string_list) law octets_to_string_list: for o: B.Octets {B.Octets.to_string(o) == B.to_string(B.Octets.to_list(o)) : String} LAWS.octets_concat_nil (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_concat_nil) law octets_concat_nil: {B.Octets.concat(Nil{}) == B.Octets.empty() : B.Octets} LAWS.octets_concat_cons (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_concat_cons) law octets_concat_cons: for h: B.Octets for t: List<&2, B.Octets> {B.Octets.concat(Con{h, t}) == B.Octets.append(h, B.Octets.concat(t)) : B.Octets} LAWS.octets_len_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_append) law octets_len_append: for +a: B.Octets for +b: B.Octets {B.Octets.len(B.Octets.append(a, b)) == Nat.add(B.Octets.len(a), B.Octets.len(b)) : Nat} LAWS.octets_len_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_take) law octets_len_take: for +n: Nat for +o: B.Octets {B.Octets.len(B.Octets.take(n, o)) == Nat.min(n, B.Octets.len(o)) : Nat} LAWS.octets_len_take_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_take_le) law octets_len_take_le: for +n: Nat for +o: B.Octets for h: {Nat.is_le(n, B.Octets.len(o)) == True{} : Bool} {B.Octets.len(B.Octets.take(n, o)) == n : Nat} LAWS.octets_len_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_drop) law octets_len_drop: for +n: Nat for +o: B.Octets {B.Octets.len(B.Octets.drop(n, o)) == Nat.sub(B.Octets.len(o), n) : Nat} LAWS.octets_len_slice (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_slice) law octets_len_slice: for +i: Nat for +n: Nat for +o: B.Octets {B.Octets.len(B.Octets.slice(i, n, o)) == Nat.min(n, Nat.sub(B.Octets.len(o), i)) : Nat} LAWS.octets_len_slice_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_slice_le) law octets_len_slice_le: for +i: Nat for +n: Nat for +o: B.Octets for h: {Nat.is_le(Nat.add(i, n), B.Octets.len(o)) == True{} : Bool} {B.Octets.len(B.Octets.slice(i, n, o)) == n : Nat} LAWS.octets_len_zeros (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_zeros) law octets_len_zeros: for +n: Nat {B.Octets.len(B.Octets.zeros(n)) == n : Nat} LAWS.octets_len_of_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_of_list) law octets_len_of_list: for +xs: List<&2, U32> {B.Octets.len(B.Octets.of_list(xs)) == B.len(xs) : Nat} LAWS.octets_append_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_append_assoc) law octets_append_assoc: for +a: B.Octets for +b: B.Octets for +c: B.Octets {B.Octets.append(B.Octets.append(a, b), c) == B.Octets.append(a, B.Octets.append(b, c)) : B.Octets} LAWS.octets_append_empty_l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_append_empty_l) law octets_append_empty_l: for +o: B.Octets {B.Octets.append(B.Octets.empty(), o) == o : B.Octets} LAWS.octets_append_empty_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_append_empty_r) law octets_append_empty_r: for +o: B.Octets {B.Octets.append(o, B.Octets.empty()) == o : B.Octets} LAWS.octets_drop_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_drop_zero) law octets_drop_zero: for +o: B.Octets {B.Octets.drop(0n, o) == o : B.Octets} LAWS.octets_take_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_take_len) law octets_take_len: for +o: B.Octets {B.Octets.take(B.Octets.len(o), o) == o : B.Octets} LAWS.octets_drop_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_drop_drop) law octets_drop_drop: for +j: Nat for +i: Nat for +o: B.Octets {B.Octets.drop(i, B.Octets.drop(j, o)) == B.Octets.drop(Nat.add(j, i), o) : B.Octets} LAWS.octets_take_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_take_take) law octets_take_take: for +i: Nat for +j: Nat for +o: B.Octets {B.Octets.take(i, B.Octets.take(j, o)) == B.Octets.take(Nat.min(i, j), o) : B.Octets} LAWS.octets_take_drop_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_take_drop_comm) law octets_take_drop_comm: for +i: Nat for +j: Nat for +o: B.Octets {B.Octets.take(i, B.Octets.drop(j, o)) == B.Octets.drop(j, B.Octets.take(Nat.add(j, i), o)) : B.Octets} LAWS.octets_drop_take_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_drop_take_comm) law octets_drop_take_comm: for +i: Nat for +j: Nat for +o: B.Octets {B.Octets.drop(i, B.Octets.take(j, o)) == B.Octets.take(Nat.sub(j, i), B.Octets.drop(i, o)) : B.Octets} LAWS.octets_take_append_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_take_append_le) law octets_take_append_le: for +n: Nat for +a: B.Octets for +b: B.Octets for h: {Nat.is_le(n, B.Octets.len(a)) == True{} : Bool} {B.Octets.take(n, B.Octets.append(a, b)) == B.Octets.take(n, a) : B.Octets} LAWS.octets_take_append_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_take_append_add) law octets_take_append_add: for +a: B.Octets for +n: Nat for +b: B.Octets {B.Octets.take(Nat.add(B.Octets.len(a), n), B.Octets.append(a, b)) == B.Octets.append(a, B.Octets.take(n, b)) : B.Octets} LAWS.octets_drop_append_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_drop_append_le) law octets_drop_append_le: for +n: Nat for +a: B.Octets for +b: B.Octets for h: {Nat.is_le(n, B.Octets.len(a)) == True{} : Bool} {B.Octets.drop(n, B.Octets.append(a, b)) == B.Octets.append(B.Octets.drop(n, a), b) : B.Octets} LAWS.octets_drop_append_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_drop_append_add) law octets_drop_append_add: for +a: B.Octets for +n: Nat for +b: B.Octets {B.Octets.drop(Nat.add(B.Octets.len(a), n), B.Octets.append(a, b)) == B.Octets.drop(n, b) : B.Octets} LAWS.octets_slice_append_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_slice_append_add) law octets_slice_append_add: for +a: B.Octets for +i: Nat for +n: Nat for +b: B.Octets {B.Octets.slice(Nat.add(B.Octets.len(a), i), n, B.Octets.append(a, b)) == B.Octets.slice(i, n, b) : B.Octets} LAWS.octets_slice_append_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_slice_append_le) law octets_slice_append_le: for +i: Nat for +n: Nat for +a: B.Octets for +b: B.Octets for h: {Nat.is_le(Nat.add(i, n), B.Octets.len(a)) == True{} : Bool} {B.Octets.slice(i, n, B.Octets.append(a, b)) == B.Octets.slice(i, n, a) : B.Octets} LAWS.octets_slice_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_slice_drop) law octets_slice_drop: for +j: Nat for +i: Nat for +n: Nat for +o: B.Octets {B.Octets.slice(i, n, B.Octets.drop(j, o)) == B.Octets.slice(Nat.add(j, i), n, o) : B.Octets} LAWS.octets_slice_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_slice_take) law octets_slice_take: for +m: Nat for +i: Nat for +n: Nat for +o: B.Octets for h: {Nat.is_le(Nat.add(i, n), m) == True{} : Bool} {B.Octets.slice(i, n, B.Octets.take(m, o)) == B.Octets.slice(i, n, o) : B.Octets} LAWS.octets_at_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_at_list) law octets_at_list: for +o: B.Octets for +i: Nat {B.Octets.at(o, i) == B.at(B.Octets.to_list(o), i) : Maybe<&2, U32>} LAWS.octets_at_append_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_at_append_add) law octets_at_append_add: for +a: B.Octets for +b: B.Octets for +i: Nat {B.Octets.at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.at(b, i) : Maybe<&2, U32>} LAWS.octets_at_append_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_at_append_lt) law octets_at_append_lt: for +a: B.Octets for +b: B.Octets for +i: Nat for h: {Nat.is_lt(i, B.Octets.len(a)) == True{} : Bool} {B.Octets.at(B.Octets.append(a, b), i) == B.Octets.at(a, i) : Maybe<&2, U32>} LAWS.octets_at_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_at_drop) law octets_at_drop: for +j: Nat for +o: B.Octets for +i: Nat {B.Octets.at(B.Octets.drop(j, o), i) == B.Octets.at(o, Nat.add(j, i)) : Maybe<&2, U32>} LAWS.octets_at_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_at_take) law octets_at_take: for +n: Nat for +o: B.Octets for +i: Nat for h: {Nat.is_lt(i, n) == True{} : Bool} {B.Octets.at(B.Octets.take(n, o), i) == B.Octets.at(o, i) : Maybe<&2, U32>} LAWS.at_append_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=at_append_add) law at_append_add: for +a: List<&2, U32> for +b: List<&2, U32> for +i: Nat {B.at(B.append(a, b), Nat.add(B.len(a), i)) == B.at(b, i) : Maybe<&2, U32>} LAWS.at_append_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=at_append_lt) law at_append_lt: for +a: List<&2, U32> for +b: List<&2, U32> for +i: Nat for h: {Nat.is_lt(i, B.len(a)) == True{} : Bool} {B.at(B.append(a, b), i) == B.at(a, i) : Maybe<&2, U32>} LAWS.at_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=at_drop) law at_drop: for +j: Nat for +xs: List<&2, U32> for +i: Nat {B.at(B.drop(j, xs), i) == B.at(xs, Nat.add(j, i)) : Maybe<&2, U32>} LAWS.at_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=at_take) law at_take: for +n: Nat for +xs: List<&2, U32> for +i: Nat for h: {Nat.is_lt(i, n) == True{} : Bool} {B.at(B.take(n, xs), i) == B.at(xs, i) : Maybe<&2, U32>} LAWS.octets_len_le16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_le16) law octets_len_le16: for +v: U32 {B.Octets.len(B.Octets.le16(v)) == 2n : Nat} LAWS.octets_len_be16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_be16) law octets_len_be16: for +v: U32 {B.Octets.len(B.Octets.be16(v)) == 2n : Nat} LAWS.octets_len_le32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_le32) law octets_len_le32: for +v: U32 {B.Octets.len(B.Octets.le32(v)) == 4n : Nat} LAWS.octets_len_be32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_be32) law octets_len_be32: for +v: U32 {B.Octets.len(B.Octets.be32(v)) == 4n : Nat} LAWS.octets_len_le64 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_le64) law octets_len_le64: for +v: W.W64 {B.Octets.len(B.Octets.le64(v)) == 8n : Nat} LAWS.octets_len_be64 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_be64) law octets_len_be64: for +v: W.W64 {B.Octets.len(B.Octets.be64(v)) == 8n : Nat} LAWS.octets_le16_at_append_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le16_at_append_add) law octets_le16_at_append_add: for +a: B.Octets for +b: B.Octets for +i: Nat {B.Octets.le16_at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.le16_at(b, i) : Maybe<&2, U32>} LAWS.octets_le16_at_append_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le16_at_append_le) law octets_le16_at_append_le: for +a: B.Octets for +b: B.Octets for +i: Nat for h: {Nat.is_le(Nat.add(i, 2n), B.Octets.len(a)) == True{} : Bool} {B.Octets.le16_at(B.Octets.append(a, b), i) == B.Octets.le16_at(a, i) : Maybe<&2, U32>} LAWS.octets_le16_at_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le16_at_drop) law octets_le16_at_drop: for +j: Nat for +o: B.Octets for +i: Nat {B.Octets.le16_at(B.Octets.drop(j, o), i) == B.Octets.le16_at(o, Nat.add(j, i)) : Maybe<&2, U32>} LAWS.octets_le16_at_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_le16_at_take) law octets_le16_at_take: for +n: Nat for +o: B.Octets for +i: Nat for h: {Nat.is_le(Nat.add(i, 2n), n) == True{} : Bool} {B.Octets.le16_at(B.Octets.take(n, o), i) == B.Octets.le16_at(o, i) : Maybe<&2, U32>} LAWS.octets_be16_at_append_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_be16_at_append_add) law octets_be16_at_append_add: for +a: B.Octets for +b: B.Octets for +i: Nat {B.Octets.be16_at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.be16_at(b, i) : Maybe<&2, U32>} LAWS.octets_be16_at_append_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_be16_at_append_le) law octets_be16_at_append_le: for +a: B.Octets for +b: B.Octets for +i: Nat for h: {Nat.is_le(Nat.add(i, 2n), B.Octets.len(a)) == True{} : Bool} {B.Octets.be16_at(B.Octets.append(a, b), i) == B.Octets.be16_at(a, i) : Maybe<&2, U32>} LAWS.octets_be16_at_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_be16_at_drop) law octets_be16_at_drop: for +j: Nat for +o: B.Octets for +i: Nat {B.Octets.be16_at(B.Octets.drop(j, o), i) == B.Octets.be16_at(o, Nat.add(j, i)) : Maybe<&2, U32>} LAWS.octets_be16_at_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_be16_at_take) law octets_be16_at_take: for +n: Nat for +o: B.Octets for +i: Nat for h: {Nat.is_le(Nat.add(i, 2n), n) == True{} : Bool} {B.Octets.be16_at(B.Octets.take(n, o), i) == B.Octets.be16_at(o, i) : Maybe<&2, U32>} More: https://jend.leeeet.dev/packages/bend-osdev-bytes.txt?definitions_offset=100