src/tensor/core_LAWS.bend
bendtorch-core@0.1.0.0 · 315 lines · 42 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
4import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
5import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
6import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
7import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
8import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
9import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Projection
10
11def IndependentMapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic,
12 result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>) -> Type:
13 (inputs, outcome) = result
14 match outcome:
15 case Fail{error}:
16 Unit
17 case Done{output}:
18 @+index: U32 -> @inside: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) ->
19 {Core.observe_dynamic(output, index) == Projection.specified_expected(operation, left, right, Projection.offset_spec(plan, U32.to_nat(index))) : Maybe<&2, F32>}
20
21type IndependentModel<-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic,
22 -result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>> is Data:
23 IndependentModel{-mapping: IndependentMapping(operation, plan, left, right, result)}
24
25def IndependentPlanned(+operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic,
26 result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
27 plan: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>) -> Type:
28 match plan:
29 case Fail{error}:
30 Unit
31 case Done{+plan}:
32 IndependentMapping(operation, plan, left, right, result)
33
34type IndependentBinaryModel<-operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic,
35 -result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>> is Data:
36 IndependentBinaryModel{-mapping: IndependentPlanned(operation, left, right, result, Elementwise.plan_for(left, right))}
37
38law scalar_add:
39 for +left: F32
40 for +right: F32
41 {Elementwise.scalar(Elementwise.Add{}, left, right) == F32.add(left, right) : F32}
42
43law scalar_sub:
44 for +left: F32
45 for +right: F32
46 {Elementwise.scalar(Elementwise.Sub{}, left, right) == F32.sub(left, right) : F32}
47
48law scalar_mul:
49 for +left: F32
50 for +right: F32
51 {Elementwise.scalar(Elementwise.Mul{}, left, right) == F32.mul(left, right) : F32}
52
53law indexed_length:
54 for +shape: Shape.Shape
55 for tensor: Core.Tensor<shape>
56 Core.LengthValid<shape, tensor>
57
58law successful_construction_dimensions:
59 for +dimensions: List<&2, U32>
60 for values: List<&2, F32>
61 Core.ConstructionDimensions(dimensions, Core.construct(dimensions, values))
62
63law successful_value_count:
64 for +shape: Shape.Shape
65 for +values: List<&2, F32>
66 Core.ValuesCount(shape, values, Core.from_values(shape, values))
67
68law checked_reader_pair:
69 for +shape: Shape.Shape
70 for original: Core.Tensor<shape>
71 for +index: U32
72 Core.Read<shape, original, index>
73
74law reader_certificate_value:
75 for +shape: Shape.Shape
76 for original: Core.Tensor<shape>
77 for +index: U32
78 for certificate: Core.Read<shape, original, index>
79 {Core.read_value(shape, Core.read_flat(shape, original, index)) ==
80 Core.certificate_value(shape, original, index, certificate) : Maybe<&2, F32>}
81
82law checked_reader_source:
83 for +shape: Shape.Shape
84 for original: Core.Tensor<shape>
85 for +index: U32
86 Core.SourceRead<shape, original, index>
87
88law checked_dynamic_reader_source:
89 for original: Core.Dynamic
90 for +index: U32
91 Core.DynamicSourceRead<original, index>
92
93law checked_reader_retains_source:
94 for +shape: Shape.Shape
95 for original: Core.Tensor<shape>
96 for +index: U32
97 Core.SourceReadKeeps<shape, original, index>
98
99law checked_dynamic_reader_retains_source:
100 for original: Core.Dynamic
101 for +index: U32
102 Core.DynamicSourceReadKeeps<original, index>
103
104law primitive_read_retains_elements:
105 for +depth: Nat
106 for array: Array<F32>
107 for +index: U32
108 for +other: U32
109 for balanced: Model.Balanced(F32, depth, array)
110 {Model.observe(F32, depth, Refinement.first(F32, Array.get(F32, array, index)), Refinement.route(depth, other)) ==
111 Model.observe(F32, depth, array, Refinement.route(depth, other)) : Maybe<&2, F32>}
112
113law storage_read_retains_length:
114 for storage: Storage.Storage
115 for +index: U32
116 {Lifecycle.retained_read(Storage.get(storage, index)) == Lifecycle.logical_length(storage) : Nat}
117
118law storage_write_retains_length:
119 for storage: Storage.Storage
120 for +index: U32
121 for +value: F32
122 {Lifecycle.retained_write(Storage.set(storage, index, value)) == Lifecycle.logical_length(storage) : Nat}
123
124law storage_clone_first_length:
125 for storage: Storage.Storage
126 {Lifecycle.first_length(Storage.clone(storage)) == Lifecycle.logical_length(storage) : Nat}
127
128law storage_clone_second_length:
129 for storage: Storage.Storage
130 {Lifecycle.second_length(Storage.clone(storage)) == Lifecycle.logical_length(storage) : Nat}
131
132law primitive_clone_first_elements:
133 for +depth: Nat
134 for array: Array<F32>
135 for +path: Model.Path(depth)
136 for balanced: Model.Balanced(F32, depth, array)
137 {Model.observe(F32, depth, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), path) ==
138 Model.observe(F32, depth, array, path) : Maybe<&2, F32>}
139
140law primitive_clone_second_elements:
141 for +depth: Nat
142 for array: Array<F32>
143 for +path: Model.Path(depth)
144 for balanced: Model.Balanced(F32, depth, array)
145 {Model.observe(F32, depth, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), path) ==
146 Model.observe(F32, depth, array, path) : Maybe<&2, F32>}
147
148law tensor_write_mapping:
149 for +shape: Shape.Shape
150 for +depth: Nat
151 for +length: Nat
152 for array: Array<F32>
153 for +index: U32
154 for +value: F32
155 for balanced: Model.Balanced(F32, depth, array)
156 for valid: {Storage.bounds(depth, length) == True{} : Bool}
157 for exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}
158 for allowed: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}
159 for matched: {Storage.index_matches(depth, length, index) == True{} : Bool}
160 {Core.write_observe(shape, Core.write_flat(shape,
161 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index, value), index) == Some{value} : Maybe<&2, F32>}
162
163law broadcast_step_mapping:
164 for +operation: Elementwise.Operation
165 for +shape: Shape.Shape
166 for +depth: Nat
167 for +length: Nat
168 for array: Array<F32>
169 for +index: U32
170 for left: Core.Dynamic
171 for right: Core.Dynamic
172 for +left_value: F32
173 for +right_value: F32
174 for balanced: Model.Balanced(F32, depth, array)
175 for valid: {Storage.bounds(depth, length) == True{} : Bool}
176 for exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}
177 for allowed: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}
178 for matched: {Storage.index_matches(depth, length, index) == True{} : Bool}
179 {Elementwise.step_observe(shape, Elementwise.step_right(operation, shape, index, left,
180 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, left_value,
181 (right, Done{right_value})), index) == Some{Elementwise.scalar(operation, left_value, right_value)} : Maybe<&2, F32>}
182
183law checked_route_separation:
184 for +depth: Nat
185 for +length: Nat
186 for +index: U32
187 for +other: U32
188 for index_checked: {Storage.index_matches(depth, length, index) == True{} : Bool}
189 for other_checked: {Storage.index_matches(depth, length, other) == True{} : Bool}
190 for different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool}
191 {Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)) == False{} : Bool}
192
193law tensor_write_frame:
194 for +shape: Shape.Shape
195 for +depth: Nat
196 for +length: Nat
197 for array: Array<F32>
198 for +index: U32
199 for +other: U32
200 for +value: F32
201 for balanced: Model.Balanced(F32, depth, array)
202 for valid: {Storage.bounds(depth, length) == True{} : Bool}
203 for exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}
204 for allowed: {Nat.is_lt(U32.to_nat(index), length) == True{} : Bool}
205 for index_checked: {Storage.index_matches(depth, length, index) == True{} : Bool}
206 for other_checked: {Storage.index_matches(depth, length, other) == True{} : Bool}
207 for different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool}
208 {Core.write_observe(shape, Core.write_flat(shape,
209 Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index, value), other) ==
210 Model.observe(F32, depth, array, Refinement.route(depth, other)) : Maybe<&2, F32>}
211
212law checked_conversion_value:
213 for +cursor: Nat
214 for +index: U32
215 for verdict: {True{} == Nat.is_eq(U32.to_nat(index), cursor) : Bool}
216 {U32.to_nat(index) == cursor : Nat}
217
218law natural_cursor_step:
219 for +operation: Elementwise.Operation
220 for +plan: Shape.BroadcastPlan
221 for +cursor: Nat
222 for state: Elementwise.State<Shape.output_shape(plan)>
223 Elementwise.CursorValidity(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state))
224
225law u32_natural_injective:
226 for +left: U32
227 for +right: U32
228 for equal: {U32.to_nat(left) == U32.to_nat(right) : Nat}
229 {left == right : U32}
230
231law checked_writer_pair:
232 for +shape: Shape.Shape
233 for original: Core.Tensor<shape>
234 for +index: U32
235 for +value: F32
236 Core.Write<shape, original, index, value>
237
238law checked_writer_source:
239 for +shape: Shape.Shape
240 for original: Core.Tensor<shape>
241 for +index: U32
242 for +value: F32
243 Core.CheckedUpdateModel<shape, original, index, value>
244
245law actual_elementwise_step:
246 for +operation: Elementwise.Operation
247 for +plan: Shape.BroadcastPlan
248 for +index: U32
249 for original: Elementwise.State<Shape.output_shape(plan)>
250 Elementwise.StepCertificate<operation, plan, index, original>
251
252law successful_elementwise_loop:
253 for +operation: Elementwise.Operation
254 for +plan: Shape.BroadcastPlan
255 for left: Core.Dynamic
256 for right: Core.Dynamic
257 for output: Core.Tensor<Shape.output_shape(plan)>
258 Elementwise.MappingModel<operation, plan, left, right,
259 Elementwise.loop(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, Elementwise.State{left, right, output})>
260
261law successful_elementwise_cached_loop:
262 for +operation: Elementwise.Operation
263 for +plan: Shape.BroadcastPlan
264 for left: Core.Dynamic
265 for right: Core.Dynamic
266 for output: Core.Tensor<Shape.output_shape(plan)>
267 Elementwise.MappingModel<operation, plan, left, right,
268 Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})>
269
270law successful_elementwise_allocated:
271 for +operation: Elementwise.Operation
272 for +plan: Shape.BroadcastPlan
273 for left: Core.Dynamic
274 for right: Core.Dynamic
275 Elementwise.MappingModel<operation, plan, left, right,
276 Elementwise.allocated(operation, plan, left, right, Core.new(Shape.output_shape(plan), 0.0))>
277
278law successful_elementwise_binary:
279 for +operation: Elementwise.Operation
280 for left: Core.Dynamic
281 for right: Core.Dynamic
282 Elementwise.BinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>
283
284law independent_elementwise_loop:
285 for +operation: Elementwise.Operation
286 for +plan: Shape.BroadcastPlan
287 for left: Core.Dynamic
288 for right: Core.Dynamic
289 for output: Core.Tensor<Shape.output_shape(plan)>
290 IndependentModel<operation, plan, left, right,
291 Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})>
292
293law independent_elementwise_binary:
294 for +operation: Elementwise.Operation
295 for left: Core.Dynamic
296 for right: Core.Dynamic
297 IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>
298
299law public_add_dispatch:
300 for left: Core.Dynamic
301 for right: Core.Dynamic
302 {Elementwise.add(left, right) == Elementwise.binary(Elementwise.Add{}, left, right) :
303 (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>}
304
305law public_sub_dispatch:
306 for left: Core.Dynamic
307 for right: Core.Dynamic
308 {Elementwise.sub(left, right) == Elementwise.binary(Elementwise.Sub{}, left, right) :
309 (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>}
310
311law public_mul_dispatch:
312 for left: Core.Dynamic
313 for right: Core.Dynamic
314 {Elementwise.mul(left, right) == Elementwise.binary(Elementwise.Mul{}, left, right) :
315 (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>}