array.bend

bend-osdev-array@0.1.0.1 · 69 lines · 7 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)}