LAWS.bend

lawful-arrays@0.1.0.0 · 211 lines · 21 definitions

1import Base
2import lawful-arrays@0.1.0.0/defs.bend as D
3
4# lawful-arrays: what Base's Array operations do, stated on the list of an
5# array's leaves (D.view). The laws are about perfect trees (D.full: depth d,
6# 2^d leaves), which is what Array.new makes and every operation keeps. For
7# d < 32, an index i reaches leaf i modulo 2^d (D.slot); from 32 up Base's
8# Array.size wraps to 0, so the indexing laws require d < 32. Elements are Data
9# (Array.get requires it, and so does D.view); only swap_full also covers
10# other element types.
11
12# ==========================================================================
13# Creating
14# ==========================================================================
15
16law new_full:
17  for -T: Data
18  for d: Nat
19  for v: T
20  {D.full(T, Array.new(T, d, v), d) == True{} : Bool}
21
22law new_view:
23  for -T: Data
24  for d: Nat
25  for v: T
26  {D.view(T, Array.new(T, d, v)) == List.replicate(T, Nat.pow(2n, d), v) : List<&2, T>}
27
28# ==========================================================================
29# Size
30# ==========================================================================
31
32law view_length:
33  for -T: Data
34  for a: Array<T>
35  for d: Nat
36  for hf: {D.full(T, a, d) == True{} : Bool}
37  {List.length(&2, T, D.view(T, a)) == Nat.pow(2n, d) : Nat}
38
39# Array.size doubles 1 once per level of the left spine: for a perfect tree of
40# depth d below 32 that is the number of leaves, 2^d.
41law size_count:
42  for -T: Data
43  for a: Array<T>
44  for d: Nat
45  for hf: {D.full(T, a, d) == True{} : Bool}
46  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
47  {U32.to_nat(Pair.snd(Array<T>, U32, Array.size(T, a))) == Nat.pow(2n, d) : Nat}
48
49law size_kept:
50  for -T: Data
51  for a: Array<T>
52  {Pair.fst(Array<T>, U32, Array.size(T, a)) == a : Array<T>}
53
54# ==========================================================================
55# Reading
56# ==========================================================================
57
58# Array.get reads leaf i (modulo the size).
59law get_view:
60  for -T: Data
61  for a: Array<T>
62  for d: Nat
63  for i: U32
64  for hf: {D.full(T, a, d) == True{} : Bool}
65  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
66  {Some{Pair.snd(Array<T>, T, Array.get(T, a, i))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}
67
68# Array.get hands back the same array.
69law get_kept:
70  for -T: Data
71  for a: Array<T>
72  for i: U32
73  {Pair.fst(Array<T>, T, Array.get(T, a, i)) == a : Array<T>}
74
75# ==========================================================================
76# Writing
77# ==========================================================================
78
79# Array.set replaces leaf i (modulo the size) and nothing else.
80law set_view:
81  for -T: Data
82  for a: Array<T>
83  for d: Nat
84  for i: U32
85  for v: T
86  for hf: {D.full(T, a, d) == True{} : Bool}
87  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
88  {D.view(T, Array.set(T, a, i, v)) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>}
89
90law set_full:
91  for -T: Data
92  for a: Array<T>
93  for d: Nat
94  for i: U32
95  for v: T
96  for hf: {D.full(T, a, d) == True{} : Bool}
97  {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool}
98
99# Reading what was just written gives it back.
100# (This holds for every tree: set and get take the same path.)
101law get_set_same:
102  for -T: Data
103  for a: Array<T>
104  for i: U32
105  for v: T
106  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}
107
108# Writing leaf i does not change leaf j (j a different leaf modulo the size).
109law get_set_other:
110  for -T: Data
111  for a: Array<T>
112  for d: Nat
113  for i: U32
114  for j: U32
115  for v: T
116  for hf: {D.full(T, a, d) == True{} : Bool}
117  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
118  for hij: {Nat.is_eq(D.slot(i, d), D.slot(j, d)) == False{} : Bool}
119  {Pair.snd(Array<T>, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array<T>, T, Array.get(T, a, j)) : T}
120
121# ==========================================================================
122# Swapping (Array.set is a swap that drops the old value; for elements that
123# are not Data only swap_full applies)
124# ==========================================================================
125
126law swap_view:
127  for -T: Data
128  for a: Array<T>
129  for d: Nat
130  for i: U32
131  for v: T
132  for hf: {D.full(T, a, d) == True{} : Bool}
133  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
134  {D.view(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v))) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>}
135
136law swap_old:
137  for -T: Data
138  for a: Array<T>
139  for d: Nat
140  for i: U32
141  for v: T
142  for hf: {D.full(T, a, d) == True{} : Bool}
143  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
144  {Some{Pair.snd(Array<T>, T, Array.swap(T, a, i, v))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}
145
146law swap_full:
147  for -T: Type
148  for a: Array<T>
149  for d: Nat
150  for i: U32
151  for v: T
152  for hf: {D.full(T, a, d) == True{} : Bool}
153  {D.full(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v)), d) == True{} : Bool}
154
155# ==========================================================================
156# Shapes, equality and indexes
157# ==========================================================================
158
159# Two perfect trees of the same depth with the same leaves are the same array.
160law view_inj:
161  for -T: Data
162  for a: Array<T>
163  for b: Array<T>
164  for d: Nat
165  for ha: {D.full(T, a, d) == True{} : Bool}
166  for hb: {D.full(T, b, d) == True{} : Bool}
167  for h: {D.view(T, a) == D.view(T, b) : List<&2, T>}
168  {a == b : Array<T>}
169
170# Array.get as a literal pair (so code that destructures it can be rewritten).
171law get_pair:
172  for -T: Data
173  for a: Array<T>
174  for i: U32
175  {Array.get(T, a, i) == (a, Pair.snd(Array<T>, T, Array.get(T, a, i))) : Array<T> & T}
176
177law size_pair:
178  for -T: Data
179  for a: Array<T>
180  for d: Nat
181  for hf: {D.full(T, a, d) == True{} : Bool}
182  {Array.size(T, a) == (a, U32.shln(1, d)) : Array<T> & U32}
183
184# A new array reads as its initial value everywhere (every depth, every index).
185law get_new:
186  for -T: Data
187  for d: Nat
188  for v: T
189  for i: U32
190  {Pair.snd(Array<T>, T, Array.get(T, Array.new(T, d, v), i)) == v : T}
191
192law slot_lt:
193  for i: U32
194  for d: Nat
195  {Nat.is_lt(D.slot(i, d), Nat.pow(2n, d)) == True{} : Bool}
196
197law slot_small:
198  for i: U32
199  for d: Nat
200  for h: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool}
201  {D.slot(i, d) == U32.to_nat(i) : Nat}
202
203# ==========================================================================
204# Cloning
205# ==========================================================================
206
207# Array.clone gives two arrays equal to the original.
208law clone_pair:
209  for -T: Data
210  for a: Array<T>
211  {Array.clone(T, a) == (a, a) : Array<T> & Array<T>}