bend-osdev-array

Releases (2)

• 0.1.0.1 indexed
• 0.1.0.0 unindexed

Definitions (227)

array.bend

• def Arrays.slots2^d, the slot count of an array of depth d
• def Arrays.is_perfectwhether a is a perfect tree of depth d (every leaf at depth d), the shape Array.new builds and Array.set keeps
• def Arrays.leavesthe slots of an array, in index order: the list model the laws compare Array.get and Array.set with (a specification: it walks the whole array)
• def Arrays.indexthe slot that Array.get and Array.set use for index i on an array of depth d: i masked to its low d bits, as Base computes it
• def Arrays.nth.orThe list model's element at slot k, or fill past its end
• def Arrays.nth
• def Arrays.of_listThe perfect array of depth d whose slots are xs in order (cut to 2^d slots, or padded with fill): an array built from a Data list, so that a proof can name it as often as it likes (a specification, like leaves)

check.bend

• def show_list
• def samplea depth-3 array (8 slots) with slots 1, 5 and 6 written (14 wraps to 6)
• def reads.gothe reads of indices from i on, n of them (r: the read of index i)
• def reads
• def main

PROOF.bend

• def AP.reflect_list
• def AP.ol_sym
• def AP.of_list_get.go
• def AP.of_list_set.go
• def AP.of_list_size.go
• def AP.reflect.go
• def AP.wh0
• def AP.whbv(b, x) = 2s + k: k is bv(b, x - s)
• def AP.wh2bv(b, x) = 2s + k: x is s + (x - s)
• def AP.lt_rw_k
• def AP.wrapa word of value 2^d + k, k < 2^d, masked to its low d bits, is k
• def AP.u32_wrap
• def AP.wrap_lts + k < 2s, for k < s
• def AP.index_wrap.go
• def AP.index_of_u32.go