array.bend
bend-osdev-array@0.1.0.0 · 69 lines · 0 definitions
1# bend-osdev-array: laws about Base's Array, the specification they are
2# stated in, and the list model they are stated against.
3#
4# Base defines Array<T> in Bend itself, as a tree of ALeaf / ANode, and
5# indexes it by U32 (Array.size, Array.swap, Array.set, Array.get, Array.new).
6# An array built by Array.new(T, d, v) is a perfect tree of depth d: 2^d
7# slots, every leaf at depth d. Array.get and Array.set mask the index to its
8# low d bits, so they read and write slot `Arrays.index(d, i)`.
9#
10# This file holds only the vocabulary the laws use; LAWS.bend states them and
11# PROOF.bend proves them.
12import Base
13
14# 2^d, the slot count of an array of depth d
15def Arrays.slots(d: Nat) -> Nat:
16 match d:
17 case 0n:
18 1n
19 case 1n+p:
20 Nat.double(Arrays.slots(p))
21
22# whether a is a perfect tree of depth d (every leaf at depth d), the shape
23# Array.new builds and Array.set keeps
24def Arrays.is_perfect(-T: Type, +d: Nat, a: Array<T>) -> Bool:
25 match d a:
26 case 0n ALeaf{x}:
27 True{}
28 case 0n ANode{xs, ys}:
29 False{}
30 case 1n+p ALeaf{x}:
31 False{}
32 case 1n+p ANode{xs, ys}:
33 Bool.and(Arrays.is_perfect(T, p, xs), Arrays.is_perfect(T, p, ys))
34
35# the slots of an array, in index order: the list model the laws compare
36# Array.get and Array.set with (a specification: it walks the whole array)
37def Arrays.leaves(-T: Data, a: Array<T>) -> List<&2, T>:
38 match a:
39 case ALeaf{x}:
40 Con{x, Nil{}}
41 case ANode{xs, ys}:
42 List.append(&2, T, Arrays.leaves(T, xs), Arrays.leaves(T, ys))
43
44# the slot that Array.get and Array.set use for index i on an array of depth
45# d: i masked to its low d bits, as Base computes it
46def Arrays.index(d: Nat, i: U32) -> Nat:
47 U32.to_nat(U32.and(i, U32.sub(U32.shln(1, d), 1)))
48
49# The list model's element at slot k, or fill past its end
50def Arrays.nth.or(-T: Data, m: Maybe<&2, T>, fill: T) -> T:
51 match m:
52 case Some{x}:
53 x
54 case None{}:
55 fill
56
57def Arrays.nth(-T: Data, xs: List<&2, T>, k: Nat, fill: T) -> T:
58 Arrays.nth.or(T, List.get(&2, T, xs, k), fill)
59
60# The perfect array of depth d whose slots are xs in order (cut to 2^d
61# slots, or padded with fill): an array built from a Data list, so that a
62# proof can name it as often as it likes (a specification, like leaves)
63def Arrays.of_list(-T: Data, +d: Nat, +xs: List<&2, T>, +fill: T) -> Array<T>:
64 match d:
65 case 0n:
66 ALeaf{Arrays.nth(T, xs, 0n, fill)}
67 case 1n+p:
68 +s = Arrays.slots(p)
69 ANode{Arrays.of_list(T, p, List.take(&2, T, xs, s), fill), Arrays.of_list(T, p, List.drop(&2, T, xs, s), fill)}