src/storage/LAWS.bend
bendtorch-core@0.1.0.0 · 215 lines · 33 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
3import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
4import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
5import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
6
7law write_read:
8 for -T: Data
9 for +d: Nat
10 for array: Array<T>
11 for +path: Model.Path(d)
12 for value: T
13 for valid: Model.Balanced(T, d, array)
14 {Model.observe(T, d, ArrayCore.write_path(T, d, array, path, value), path) == Some{value} : Maybe<&2, T>}
15
16law update_frame:
17 for -T: Data
18 for +d: Nat
19 for array: Array<T>
20 for +i: Model.Path(d)
21 for +j: Model.Path(d)
22 for +value: T
23 for valid: Model.Balanced(T, d, array)
24 {Model.observe(T, d, ArrayCore.write_path(T, d, array, i, value), j) == Model.select(T, Model.same(d, i, j), value, Model.observe(T, d, array, j)) : Maybe<&2, T>}
25
26law read_refines:
27 for -T: Data
28 for +d: Nat
29 for array: Array<T>
30 for +path: Model.Path(d)
31 for valid: Model.Balanced(T, d, array)
32 {ArrayCore.observation(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) == Model.observe(T, d, array, path) : Maybe<&2, T>}
33
34law read_retains:
35 for -T: Data
36 for +d: Nat
37 for array: Array<T>
38 for +path: Model.Path(d)
39 for valid: Model.Balanced(T, d, array)
40 {ArrayCore.retained(T, d, array, path, ArrayCore.read_path(T, d, array, path, valid)) == array : Array<T>}
41
42law primitive_update_frame:
43 for -T: Data
44 for +d: Nat
45 for array: Array<T>
46 for +i: U32
47 for +other: Model.Path(d)
48 for +value: T
49 for valid: Model.Balanced(T, d, array)
50 {Model.observe(T, d, Array.set(T, array, i, value), other) == Model.select(T, Model.same(d, Refinement.route(d, i), other), value, Model.observe(T, d, array, other)) : Maybe<&2, T>}
51
52law path_self_same:
53 for +d: Nat
54 for +path: Model.Path(d)
55 {Model.same(d, path, path) == True{} : Bool}
56
57law primitive_write_read:
58 for -T: Data
59 for +d: Nat
60 for array: Array<T>
61 for +i: U32
62 for +value: T
63 for valid: Model.Balanced(T, d, array)
64 {Model.observe(T, d, Array.set(T, array, i, value), Refinement.route(d, i)) == Some{value} : Maybe<&2, T>}
65
66def outcome(-A: Type, pair: Storage.Storage & A) -> A:
67 (storage, result) = pair
68 result
69
70def size(storage: Storage.Storage) -> Nat:
71 outcome(Nat, Storage.length(storage))
72
73def owner(-A: Type, pair: Storage.Storage & A) -> Storage.Storage:
74 (storage, result) = pair
75 storage
76
77def read(storage: Storage.Storage, +i: U32) -> Result<&2, &2, Storage.Error, F32>:
78 outcome(Result<&2, &2, Storage.Error, F32>, Storage.get(storage, i))
79
80def kept(storage: Storage.Storage, +i: U32) -> Storage.Storage:
81 owner(Result<&2, &2, Storage.Error, F32>, Storage.get(storage, i))
82
83def written(storage: Storage.Storage, +i: U32, value: F32) -> Storage.Storage:
84 owner(Result<&2, &2, Storage.Error, Unit>, Storage.set(storage, i, value))
85
86def status(storage: Storage.Storage, +i: U32, value: F32) -> Result<&2, &2, Storage.Error, Unit>:
87 outcome(Result<&2, &2, Storage.Error, Unit>, Storage.set(storage, i, value))
88
89def created.of(result: Result<&2, &1, Storage.Error, Storage.Storage>) -> Storage.Storage:
90 match result:
91 case Fail{error}:
92 Storage.Empty{}
93 case Done{storage}:
94 storage
95
96def created(+n: U32, value: F32) -> Storage.Storage:
97 created.of(Storage.new(n, value))
98
99def refused.of(result: Result<&2, &1, Storage.Error, Storage.Storage>) -> Maybe<&2, Storage.Error>:
100 match result:
101 case Fail{error}:
102 Some{error}
103 case Done{storage}:
104 None{}
105
106def refused(+n: U32, value: F32) -> Maybe<&2, Storage.Error>:
107 refused.of(Storage.new(n, value))
108
109def first(storage: Storage.Storage) -> Storage.Storage:
110 owner(Storage.Storage, Storage.clone(storage))
111
112def second(storage: Storage.Storage) -> Storage.Storage:
113 outcome(Storage.Storage, Storage.clone(storage))
114
115type Op is Data:
116 Write{index: U32, value: F32}
117 Read{index: U32}
118 First{}
119 Second{}
120 Length{}
121
122def step(storage: Storage.Storage, op: Op) -> Storage.Storage:
123 match op:
124 case Write{+i, value}:
125 written(storage, i, value)
126 case Read{+i}:
127 kept(storage, i)
128 case First{}:
129 first(storage)
130 case Second{}:
131 second(storage)
132 case Length{}:
133 owner(Nat, Storage.length(storage))
134
135def replay(ops: List<&2, Op>, storage: Storage.Storage) -> Storage.Storage:
136 match ops:
137 case Nil{}:
138 storage
139 case op <> rest:
140 replay(rest, step(storage, op))
141
142def latest(+n: Nat, op: Op, +j: U32, value: F32) -> F32:
143 match op:
144 case Write{+i, new}:
145 Bool.pick(F32, Bool.and(Nat.is_lt(U32.to_nat(i), n), Nat.is_eq(U32.to_nat(i), U32.to_nat(j))), new, value)
146 case Read{i}:
147 value
148 case First{}:
149 value
150 case Second{}:
151 value
152 case Length{}:
153 value
154
155def expected(ops: List<&2, Op>, +n: Nat, +j: U32, value: F32) -> F32:
156 match ops:
157 case Nil{}:
158 value
159 case op <> rest:
160 expected(rest, n, j, latest(n, op, j, value))
161
162law new_too_large:
163 for +n: U32
164 for value: F32
165 for +over: {U32.is_le(n, 1048576) == False{} : Bool}
166 {refused(n, value) == Some{Storage.TooLarge{}} : Maybe<&2, Storage.Error>}
167
168law new_fits:
169 for +n: U32
170 for value: F32
171 for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
172 {refused(n, value) == None{} : Maybe<&2, Storage.Error>}
173
174law new_empty:
175 for value: F32
176 {Storage.new(0, value) == Done{Storage.Empty{}} : Result<&2, &1, Storage.Error, Storage.Storage>}
177
178law get_outside:
179 for storage: Storage.Storage
180 for +i: U32
181 for outside: {Nat.is_lt(U32.to_nat(i), size(storage)) == False{} : Bool}
182 {read(storage, i) == Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, F32>}
183
184law set_outside:
185 for storage: Storage.Storage
186 for +i: U32
187 for value: F32
188 for outside: {Nat.is_lt(U32.to_nat(i), size(storage)) == False{} : Bool}
189 {status(storage, i, value) == Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, Unit>}
190
191law replay_size:
192 for +n: U32
193 for +value: F32
194 for +ops: List<&2, Op>
195 for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
196 {size(replay(ops, created(n, value))) == U32.to_nat(n) : Nat}
197
198law replay_get:
199 for +n: U32
200 for +value: F32
201 for +ops: List<&2, Op>
202 for +j: U32
203 for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
204 for inside: {Nat.is_lt(U32.to_nat(j), U32.to_nat(n)) == True{} : Bool}
205 {read(replay(ops, created(n, value)), j) == Done{expected(ops, U32.to_nat(n), j, value)} : Result<&2, &2, Storage.Error, F32>}
206
207law replay_set:
208 for +n: U32
209 for +value: F32
210 for +ops: List<&2, Op>
211 for +j: U32
212 for +w: F32
213 for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
214 for inside: {Nat.is_lt(U32.to_nat(j), U32.to_nat(n)) == True{} : Bool}
215 {status(replay(ops, created(n, value)), j, w) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}