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.
12	import Base
13	
14	# 2^d, the slot count of an array of depth d
15	def 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
24	def 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)
37	def 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
46	def 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
50	def 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	
57	def 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)
63	def 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)}