bend-osdev-algo

Releases (1):
  0.1.0.0  0xaca75f7679c88e3442b04b98baf3b711  indexed  https://jend.leeeet.dev/files.txt?path=bend-osdev-algo@0.1.0.0

Definitions (367, 1 to 100 shown):
  LAWS.popcount_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=popcount_le)
   law popcount_le:
     for x: U32
     {Nat.is_le(A.bits32.popcount(x), 32n) == True{} : Bool}
  LAWS.popcount_not (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=popcount_not)
   law popcount_not:
     for x: U32
     {Nat.add(A.bits32.popcount(x), A.bits32.popcount(U32.not(x))) == 32n : Nat}
  LAWS.first_set_is_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=first_set_is_set)
   law first_set_is_set:
     for x: U32
     for k: Nat
     for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
     {A.bits32.test(x, k) == True{} : Bool}
  LAWS.first_set_lowest (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=first_set_lowest)
   law first_set_lowest:
     for x: U32
     for k: Nat
     for j: Nat
     for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
     for l: {Nat.is_lt(j, k) == True{} : Bool}
     {A.bits32.test(x, j) == False{} : Bool}
  LAWS.first_set_none (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=first_set_none)
   law first_set_none:
     for x: U32
     for e: {A.bits32.first_set(x) == None{} : Maybe<&2, Nat>}
     {x == 0 : U32}
  LAWS.last_set_is_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=last_set_is_set)
   law last_set_is_set:
     for x: U32
     for k: Nat
     for e: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
     {A.bits32.test(x, k) == True{} : Bool}
  LAWS.last_set_highest (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=last_set_highest)
   law last_set_highest:
     for x: U32
     for k: Nat
     for j: Nat
     for e: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
     for l: {Nat.is_lt(k, j) == True{} : Bool}
     {A.bits32.test(x, j) == False{} : Bool}
  LAWS.last_set_none (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=last_set_none)
   law last_set_none:
     for x: U32
     for e: {A.bits32.last_set(x) == None{} : Maybe<&2, Nat>}
     {x == 0 : U32}
  LAWS.ctz_first_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=ctz_first_set)
   law ctz_first_set:
     for x: U32
     for k: Nat
     for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
     {A.bits32.ctz(x) == k : Nat}
  LAWS.clz_last_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=clz_last_set)
   law clz_last_set:
     for x: U32
     for k: Nat
     for e: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
     {Nat.add(A.bits32.clz(x), k) == 31n : Nat}
  LAWS.first_le_last (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=first_le_last)
   law first_le_last:
     for x: U32
     for i: Nat
     for k: Nat
     for e: {A.bits32.first_set(x) == Some{i} : Maybe<&2, Nat>}
     for f: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
     {Nat.is_le(i, k) == True{} : Bool}
  LAWS.ctz_clz (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=ctz_clz)
   law ctz_clz:
     for x: U32
     for k: Nat
     for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
     {Nat.is_le(Nat.add(A.bits32.ctz(x), A.bits32.clz(x)), 31n) == True{} : Bool}
  LAWS.popcount64_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=popcount64_le)
   law popcount64_le:
     for a: W.W64
     {Nat.is_le(A.bits64.popcount(a), 64n) == True{} : Bool}
  LAWS.first_set64_is_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=first_set64_is_set)
   law first_set64_is_set:
     for a: W.W64
     for k: Nat
     for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
     {A.bits64.test(a, k) == True{} : Bool}
  LAWS.first_set64_lowest (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=first_set64_lowest)
   law first_set64_lowest:
     for a: W.W64
     for k: Nat
     for j: Nat
     for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
     for l: {Nat.is_lt(j, k) == True{} : Bool}
     {A.bits64.test(a, j) == False{} : Bool}
  LAWS.first_set64_none (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=first_set64_none)
   law first_set64_none:
     for a: W.W64
     for e: {A.bits64.first_set(a) == None{} : Maybe<&2, Nat>}
     {a == W.W64.zero() : W.W64}
  LAWS.last_set64_is_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=last_set64_is_set)
   law last_set64_is_set:
     for a: W.W64
     for k: Nat
     for e: {A.bits64.last_set(a) == Some{k} : Maybe<&2, Nat>}
     {A.bits64.test(a, k) == True{} : Bool}
  LAWS.last_set64_highest (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=last_set64_highest)
   law last_set64_highest:
     for a: W.W64
     for k: Nat
     for j: Nat
     for e: {A.bits64.last_set(a) == Some{k} : Maybe<&2, Nat>}
     for l: {Nat.is_lt(k, j) == True{} : Bool}
     {A.bits64.test(a, j) == False{} : Bool}
  LAWS.ctz64_first_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=ctz64_first_set)
   law ctz64_first_set:
     for a: W.W64
     for k: Nat
     for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
     {A.bits64.ctz(a) == k : Nat}
  LAWS.clz64_last_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=clz64_last_set)
   law clz64_last_set:
     for a: W.W64
     for k: Nat
     for e: {A.bits64.last_set(a) == Some{k} : Maybe<&2, Nat>}
     {Nat.add(A.bits64.clz(a), k) == 63n : Nat}
  LAWS.ctz_clz64 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=ctz_clz64)
   law ctz_clz64:
     for a: W.W64
     for k: Nat
     for e: {A.bits64.first_set(a) == Some{k} : Maybe<&2, Nat>}
     {Nat.is_le(Nat.add(A.bits64.ctz(a), A.bits64.clz(a)), 63n) == True{} : Bool}
  LAWS.next_set_le_size (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=next_set_le_size)
   law next_set_le_size:
     for words: List<&2, U32>
     for size: Nat
     for start: Nat
     {Nat.is_le(M.bitmap.next_set(words, size, start), size) == True{} : Bool}
  LAWS.next_set_is_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=next_set_is_set)
   law next_set_is_set:
     for words: List<&2, U32>
     for size: Nat
     for start: Nat
     for l: {Nat.is_lt(M.bitmap.next_set(words, size, start), size) == True{} : Bool}
     {M.bitmap.test(words, M.bitmap.next_set(words, size, start)) == True{} : Bool}
  LAWS.next_set_at_least (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=next_set_at_least)
   law next_set_at_least:
     for words: List<&2, U32>
     for size: Nat
     for start: Nat
     for l: {Nat.is_lt(M.bitmap.next_set(words, size, start), size) == True{} : Bool}
     {Nat.is_le(start, M.bitmap.next_set(words, size, start)) == True{} : Bool}
  LAWS.next_set_none_before (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=next_set_none_before)
   law next_set_none_before:
     for words: List<&2, U32>
     for size: Nat
     for start: Nat
     for j: Nat
     for l: {Nat.is_le(start, j) == True{} : Bool}
     for m: {Nat.is_lt(j, M.bitmap.next_set(words, size, start)) == True{} : Bool}
     {M.bitmap.test(words, j) == False{} : Bool}
  LAWS.next_clear_le_size (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=next_clear_le_size)
   law next_clear_le_size:
     for words: List<&2, U32>
     for size: Nat
     for start: Nat
     {Nat.is_le(M.bitmap.next_clear(words, size, start), size) == True{} : Bool}
  LAWS.next_clear_is_clear (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=next_clear_is_clear)
   law next_clear_is_clear:
     for words: List<&2, U32>
     for size: Nat
     for start: Nat
     for l: {Nat.is_lt(M.bitmap.next_clear(words, size, start), size) == True{} : Bool}
     {M.bitmap.test(words, M.bitmap.next_clear(words, size, start)) == False{} : Bool}
  LAWS.next_clear_at_least (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=next_clear_at_least)
   law next_clear_at_least:
     for words: List<&2, U32>
     for size: Nat
     for start: Nat
     for l: {Nat.is_lt(M.bitmap.next_clear(words, size, start), size) == True{} : Bool}
     {Nat.is_le(start, M.bitmap.next_clear(words, size, start)) == True{} : Bool}
  LAWS.next_clear_none_before (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=next_clear_none_before)
   law next_clear_none_before:
     for words: List<&2, U32>
     for size: Nat
     for start: Nat
     for j: Nat
     for l: {Nat.is_le(start, j) == True{} : Bool}
     for m: {Nat.is_lt(j, M.bitmap.next_clear(words, size, start)) == True{} : Bool}
     {M.bitmap.test(words, j) == True{} : Bool}
  LAWS.lower_bound_le_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=lower_bound_le_length)
   law lower_bound_le_length:
     for xs: List<&2, U32>
     for key: U32
     {Nat.is_le(S.bsearch.lower_bound(xs, key), List.length(&2, U32, xs)) == True{} : Bool}
  LAWS.lower_bound_below (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=lower_bound_below)
   law lower_bound_below:
     for xs: List<&2, U32>
     for key: U32
     for i: Nat
     for x: U32
     for e: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
     for l: {Nat.is_lt(i, S.bsearch.lower_bound(xs, key)) == True{} : Bool}
     {U32.is_lt(x, key) == True{} : Bool}
  LAWS.lower_bound_above (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=lower_bound_above)
   law lower_bound_above:
     for xs: List<&2, U32>
     for key: U32
     for i: Nat
     for x: U32
     for s: {S.bsearch.sorted(xs) == True{} : Bool}
     for e: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
     for l: {Nat.is_le(S.bsearch.lower_bound(xs, key), i) == True{} : Bool}
     {U32.is_lt(x, key) == False{} : Bool}
  LAWS.find_some (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=find_some)
   law find_some:
     for xs: List<&2, U32>
     for key: U32
     for i: Nat
     for e: {S.bsearch.find(xs, key) == Some{i} : Maybe<&2, Nat>}
     {List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}
  LAWS.find_none (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=find_none)
   law find_none:
     for xs: List<&2, U32>
     for key: U32
     for i: Nat
     for x: U32
     for s: {S.bsearch.sorted(xs) == True{} : Bool}
     for e: {S.bsearch.find(xs, key) == None{} : Maybe<&2, Nat>}
     for g: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
     {U32.is_eq(x, key) == False{} : Bool}
  LAWS.algo_index_nat (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=algo_index_nat)
   def algo_index_nat(m: Maybe<&2, U32>) -> Maybe<&2, Nat>:
  LAWS.array_lower_bound_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=array_lower_bound_list)
   law array_lower_bound_list:
     for +d: Nat
     for a: Array<U32>
     for hp: {AR.Arrays.is_perfect(U32, d, a) == True{} : Bool}
     for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for n: U32
     for hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}
     for key: U32
     for hs: {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n))) == True{} : Bool}
     {U32.to_nat(Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(a, n, key))) == S.bsearch.lower_bound(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n)), key) : Nat}
  LAWS.array_lower_bound_same (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=array_lower_bound_same)
   law array_lower_bound_same:
     for +d: Nat
     for a: Array<U32>
     for hp: {AR.Arrays.is_perfect(U32, d, a) == True{} : Bool}
     for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for n: U32
     for key: U32
     {Pair.fst(Array<U32>, U32, S.bsearch.array_lower_bound(a, n, key)) == a : Array<U32>}
  LAWS.array_find_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=array_find_list)
   law array_find_list:
     for +d: Nat
     for a: Array<U32>
     for hp: {AR.Arrays.is_perfect(U32, d, a) == True{} : Bool}
     for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for n: U32
     for hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}
     for key: U32
     for hs: {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n))) == True{} : Bool}
     {algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(a, n, key))) == S.bsearch.find(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n)), key) : Maybe<&2, Nat>}
  LAWS.array_find_same (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=array_find_same)
   law array_find_same:
     for +d: Nat
     for a: Array<U32>
     for hp: {AR.Arrays.is_perfect(U32, d, a) == True{} : Bool}
     for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
     for n: U32
     for key: U32
     {Pair.fst(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(a, n, key)) == a : Array<U32>}
  LAWS.vec_popcount (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_popcount)
   law vec_popcount:
     {A.bits32.popcount(4294967295) == 32n : Nat}
  LAWS.vec_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_zero)
   law vec_zero:
     {(A.bits32.ffs(0), A.bits32.fls(0), A.bits32.ctz(0), A.bits32.clz(0)) == (0n, 0n, 32n, 32n) : Nat & Nat & Nat & Nat}
  LAWS.vec_forty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_forty)
   law vec_forty:
     {(A.bits32.ffs(40), A.bits32.fls(40), A.bits32.ctz(40), A.bits32.clz(40)) == (4n, 6n, 3n, 26n) : Nat & Nat & Nat & Nat}
  LAWS.vec_top (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_top)
   law vec_top:
     {(A.bits32.first_set(2147483648), A.bits32.last_set(1)) == (Some{31n}, Some{0n}) : Maybe<&2, Nat> & Maybe<&2, Nat>}
  LAWS.vec64_halves (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec64_halves)
   law vec64_halves:
     {(A.bits64.ctz(W.W64.from_parts(1, 0)), A.bits64.clz(W.W64.from_parts(0, 1)), A.bits64.popcount(W.W64.max())) == (32n, 63n, 64n) : Nat & Nat & Nat}
  LAWS.vec64_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec64_zero)
   law vec64_zero:
     {(A.bits64.first_set(W.W64.zero()), A.bits64.ctz(W.W64.zero())) == (None{}, 64n) : Maybe<&2, Nat> & Nat}
  LAWS.vec_next_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_next_set)
   law vec_next_set:
     {M.bitmap.next_set([0, 8], 64n, 3n) == 35n : Nat}
  LAWS.vec_next_set_none (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_next_set_none)
   law vec_next_set_none:
     {M.bitmap.next_set([0, 8], 35n, 0n) == 35n : Nat}
  LAWS.vec_next_clear (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_next_clear)
   law vec_next_clear:
     {M.bitmap.next_clear([4294967295, 1], 64n, 3n) == 33n : Nat}
  LAWS.vec_next_past_size (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_next_past_size)
   law vec_next_past_size:
     {M.bitmap.next_clear([0], 10n, 12n) == 10n : Nat}
  LAWS.vec_lower_bound (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_lower_bound)
   law vec_lower_bound:
     {(S.bsearch.lower_bound([1, 3, 3, 7, 9], 3), S.bsearch.lower_bound([1, 3, 3, 7, 9], 10), S.bsearch.find([1, 3, 3, 7, 9], 7), S.bsearch.find([1, 3, 3, 7, 9], 8)) == (1n, 5n, Some{3n}, None{}) : Nat & Nat & Maybe<&2, Nat> & Maybe<&2, Nat>}
  LAWS.vec_array_lower_bound (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_array_lower_bound)
   # the array [1, 3, 3, 7, 9, 0, 0, 0], searched in its first 5 slots
   law vec_array_lower_bound:
     {Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9), 5, 3)) == 1 : U32}
  LAWS.vec_array_lower_bound_end (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_array_lower_bound_end)
   law vec_array_lower_bound_end:
     {Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9), 5, 10)) == 5 : U32}
  LAWS.vec_array_find (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_array_find)
   law vec_array_find:
     {Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9), 5, 7)) == Some{3} : Maybe<&2, U32>}
  LAWS.vec_array_find_none (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=vec_array_find_none)
   law vec_array_find_none:
     {Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9), 5, 8)) == None{} : Maybe<&2, U32>}
  LAWS.wit_first_last (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=wit_first_last)
   # first_set and last_set answer Some (40 = 0b101000: bits 3 and 5), with a
   # j below and above; and None for zero
   law wit_first_last:
     {(A.bits32.first_set(40), Nat.is_lt(1n, 3n), A.bits32.last_set(40), Nat.is_lt(5n, 7n), A.bits32.first_set(0), A.bits32.last_set(0)) == (Some{3n}, True{}, Some{5n}, True{}, None{}, None{}) : Maybe<&2, Nat> & Bool & Maybe<&2, Nat> & Bool & Maybe<&2, Nat> & Maybe<&2, Nat>}
  LAWS.wit_first_last64 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=wit_first_last64)
   law wit_first_last64:
     {(A.bits64.first_set(W.W64.from_parts(1, 0)), A.bits64.last_set(W.W64.from_parts(1, 0)), A.bits64.first_set(W.W64.zero())) == (Some{32n}, Some{32n}, None{}) : Maybe<&2, Nat> & Maybe<&2, Nat> & Maybe<&2, Nat>}
  LAWS.wit_next (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=wit_next)
   # an answer below the size, and a j with start <= j < answer
   law wit_next:
     {(Nat.is_lt(M.bitmap.next_set([0, 8], 64n, 3n), 64n), Nat.is_le(3n, 10n), Nat.is_lt(10n, M.bitmap.next_set([0, 8], 64n, 3n)), Nat.is_lt(M.bitmap.next_clear([4294967295, 1], 64n, 3n), 64n), Nat.is_lt(10n, M.bitmap.next_clear([4294967295, 1], 64n, 3n))) == (True{}, True{}, True{}, True{}, True{}) : Bool & Bool & Bool & Bool & Bool}
  LAWS.wit_bsearch (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=wit_bsearch)
   # a sorted list; an element before the lower bound of 7 (index 1) and one
   # from it on (index 4); find answering Some and None
   law wit_bsearch:
     {(S.bsearch.sorted([1, 3, 3, 7, 9]), S.bsearch.lower_bound([1, 3, 3, 7, 9], 7), List.get(&2, U32, [1, 3, 3, 7, 9], 1n), List.get(&2, U32, [1, 3, 3, 7, 9], 4n), S.bsearch.find([1, 3, 3, 7, 9], 7), S.bsearch.find([1, 3, 3, 7, 9], 8)) == (True{}, 3n, Some{3}, Some{9}, Some{3n}, None{}) : Bool & Nat & Maybe<&2, U32> & Maybe<&2, U32> & Maybe<&2, Nat> & Maybe<&2, Nat>}
  LAWS.wit_array_bsearch (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&name=wit_array_bsearch)
   # the array [1, 3, 3, 7, 9, 0, 0, 0] (depth 3), searched in its first 5
   # slots: perfect, of depth below 32, 5 <= 2^3, and those slots sorted
   law wit_array_bsearch:
     {(AR.Arrays.is_perfect(U32, 3n, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9)), Nat.is_lt(3n, 32n), Nat.is_le(U32.to_nat(5), AR.Arrays.slots(3n)), S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, Array.set(U32, [0 : U32*8n], 0, 1), 1, 3), 2, 3), 3, 7), 4, 9)), U32.to_nat(5)))) == (True{}, True{}, True{}, True{}) : Bool & Bool & Bool & Bool}
  PROOF.absurd.bool (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=absurd.bool)
   def absurd.bool(b: Bool) -> Type:
  PROOF.absurd.tf (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=absurd.tf)
   def absurd.tf(e: {True{} == False{} : Bool}) -> Empty:
  PROOF.absurd.ft (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=absurd.ft)
   def absurd.ft(e: {False{} == True{} : Bool}) -> Empty:
  PROOF.absurd.nat (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=absurd.nat)
   def absurd.nat(n: Nat) -> Type:
  PROOF.absurd.sz (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=absurd.sz)
   def absurd.sz(-k: Nat, e: {1n+k == 0n : Nat}) -> Empty:
  PROOF.absurd.maybe (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=absurd.maybe)
   def absurd.maybe(m: Maybe<&2, Nat>) -> Type:
  PROOF.absurd.sn (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=absurd.sn)
   def absurd.sn(-k: Nat, e: {Some{k} == None{} : Maybe<&2, Nat>}) -> Empty:
  PROOF.absurd.ns (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=absurd.ns)
   def absurd.ns(-k: Nat, e: {None{} == Some{k} : Maybe<&2, Nat>}) -> Empty:
  PROOF.maybe.get (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=maybe.get)
   def maybe.get(m: Maybe<&2, Nat>) -> Nat:
  PROOF.some_inj (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=some_inj)
   def some_inj(-a: Nat, -b: Nat, e: {Some{a} == Some{b} : Maybe<&2, Nat>}) -> {a == b : Nat}:
  PROOF.nat.le_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.le_zero)
   def nat.le_zero(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
  PROOF.nat.lt_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.lt_zero)
   def nat.lt_zero(x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}:
  PROOF.nat.lt_irrefl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.lt_irrefl)
   def nat.lt_irrefl(x: Nat) -> {Nat.is_lt(x, x) == False{} : Bool}:
  PROOF.nat.le_refl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.le_refl)
   def nat.le_refl(x: Nat) -> {Nat.is_le(x, x) == True{} : Bool}:
  PROOF.nat.le_succ (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.le_succ)
   def nat.le_succ(a: Nat, b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(a, 1n+b) == True{} : Bool}:
  PROOF.nat.add_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.add_zero)
   def nat.add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
  PROOF.nat.add_succ (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.add_succ)
   def nat.add_succ(a: Nat, -b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
  PROOF.nat.sub_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.sub_add)
   # n - k + k = n, for k <= n
   def nat.sub_add(n: Nat, k: Nat, e: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.add(Nat.sub(n, k), k) == n : Nat}:
  PROOF.nat.sub_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.sub_le)
   def nat.sub_le(n: Nat, k: Nat) -> {Nat.is_le(Nat.sub(n, k), n) == True{} : Bool}:
  PROOF.nat.add_sub_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.add_sub_le)
   # k <= l <= n gives k + (n - l) <= n
   def nat.add_sub_le(k: Nat, l: Nat, n: Nat, e: {Nat.is_le(k, l) == True{} : Bool}, f: {Nat.is_le(l, n) == True{} : Bool}) -> {Nat.is_le(Nat.add(k, Nat.sub(n, l)), n) == True{} : Bool}:
  PROOF.bitw.popcount_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.popcount_le)
   def bitw.popcount_le(n: Nat, w: Word(n)) -> {Nat.is_le(A.bitw.popcount(n, w), n) == True{} : Bool}:
  PROOF.bitw.popcount_not (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.popcount_not)
   def bitw.popcount_not(n: Nat, w: Word(n)) -> {Nat.add(A.bitw.popcount(n, w), A.bitw.popcount(n, Word.not(n, w))) == n : Nat}:
  PROOF.bitw.at1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.at1)
   def bitw.at1(n: Nat, w: Word(n), m: Nat) -> Bool:
  PROOF.nat.pos (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=nat.pos)
   def nat.pos(m: Nat) -> Bool:
  PROOF.bitw.below (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.below)
   # j lies below the lowest set bit (every j does when there is none)
   def bitw.below(j: Nat, m: Nat) -> Bool:
  PROOF.bitw.above (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.above)
   # j lies above the highest set bit (every j does when there is none)
   def bitw.above(j: Nat, m: Nat) -> Bool:
  PROOF.bitw.ffs_set.h (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.ffs_set.h)
   def bitw.ffs_set.h(p: Nat, -t: Word(p), m: Nat, ih: {bitw.at1(p, t, m) == nat.pos(m) : Bool}) -> {bitw.at1(1n+p, WCon{False{}, t}, A.bitw.ffs.step(False{}, m)) == nat.pos(A.bitw.ffs.step(False{}, m)) : Bool}:
  PROOF.bitw.ffs_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.ffs_set)
   def bitw.ffs_set(n: Nat, w: Word(n)) -> {bitw.at1(n, w, A.bitw.ffs(n, w)) == nat.pos(A.bitw.ffs(n, w)) : Bool}:
  PROOF.bitw.ffs_low.z (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.ffs_low.z)
   def bitw.ffs_low.z(m: Nat) -> {Bool.and(bitw.below(0n, A.bitw.ffs.step(False{}, m)), False{}) == False{} : Bool}:
  PROOF.bitw.ffs_low.s (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.ffs_low.s)
   def bitw.ffs_low.s(-p: Nat, -t: Word(p), m: Nat, -j: Nat, ih: {Bool.and(bitw.below(j, m), A.bitw.test(p, t, j)) == False{} : Bool}) -> {Bool.and(bitw.below(1n+j, A.bitw.ffs.step(False{}, m)), A.bitw.test(1n+p, WCon{False{}, t}, 1n+j)) == False{} : Bool}:
  PROOF.bitw.ffs_low (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.ffs_low)
   def bitw.ffs_low(n: Nat, w: Word(n), j: Nat) -> {Bool.and(bitw.below(j, A.bitw.ffs(n, w)), A.bitw.test(n, w, j)) == False{} : Bool}:
  PROOF.bitw.ffs_zero.h (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.ffs_zero.h)
   def bitw.ffs_zero.h(m: Nat, e: {A.bitw.ffs.step(False{}, m) == 0n : Nat}) -> {m == 0n : Nat}:
  PROOF.bitw.ffs_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.ffs_zero)
   def bitw.ffs_zero(n: Nat, w: Word(n), e: {A.bitw.ffs(n, w) == 0n : Nat}) -> {w == Word.zero(n) : Word(n)}:
  PROOF.bitw.fls_set.h (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.fls_set.h)
   def bitw.fls_set.h(p: Nat, -t: Word(p), m: Nat, b: Bool, ih: {bitw.at1(p, t, m) == nat.pos(m) : Bool}) -> {bitw.at1(1n+p, WCon{b, t}, A.bitw.fls.step(m, b)) == nat.pos(A.bitw.fls.step(m, b)) : Bool}:
  PROOF.bitw.fls_set (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.fls_set)
   def bitw.fls_set(n: Nat, w: Word(n)) -> {bitw.at1(n, w, A.bitw.fls(n, w)) == nat.pos(A.bitw.fls(n, w)) : Bool}:
  PROOF.bitw.fls_high.z (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.fls_high.z)
   def bitw.fls_high.z(m: Nat, b: Bool) -> {Bool.and(bitw.above(0n, A.bitw.fls.step(m, b)), b) == False{} : Bool}:
  PROOF.bitw.fls_high.s (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.fls_high.s)
   def bitw.fls_high.s(-p: Nat, -t: Word(p), m: Nat, b: Bool, -j: Nat, ih: {Bool.and(bitw.above(j, m), A.bitw.test(p, t, j)) == False{} : Bool}) -> {Bool.and(bitw.above(1n+j, A.bitw.fls.step(m, b)), A.bitw.test(1n+p, WCon{b, t}, 1n+j)) == False{} : Bool}:
  PROOF.bitw.fls_high (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.fls_high)
   def bitw.fls_high(n: Nat, w: Word(n), j: Nat) -> {Bool.and(bitw.above(j, A.bitw.fls(n, w)), A.bitw.test(n, w, j)) == False{} : Bool}:
  PROOF.bitw.fls_zero.m (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.fls_zero.m)
   def bitw.fls_zero.m(m: Nat, b: Bool, e: {A.bitw.fls.step(m, b) == 0n : Nat}) -> {m == 0n : Nat}:
  PROOF.bitw.fls_zero.b (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.fls_zero.b)
   def bitw.fls_zero.b(m: Nat, b: Bool, e: {A.bitw.fls.step(m, b) == 0n : Nat}) -> {b == False{} : Bool}:
  PROOF.bitw.fls_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bitw.fls_zero)
   def bitw.fls_zero(n: Nat, w: Word(n), e: {A.bitw.fls(n, w) == 0n : Nat}) -> {w == Word.zero(n) : Word(n)}:
More: https://jend.leeeet.dev/packages/bend-osdev-algo.txt?definitions_offset=100