1	import Base
2	import ../shape/core.bend as Shape
3	import ../storage/main.bend as Storage
4	import ../storage/model.bend as Model
5	import ../storage/refinement.bend as Refinement
6	import ./core.bend as Core
7	import ./lifecycle.bend as Lifecycle
8	import ./elementwise.bend as Elementwise
9	import ./projection_LAWS.bend as Projection
10	
11	def 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	
21	type 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	
25	def 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	
34	type 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	
38	law scalar_add:
39	  for +left: F32
40	  for +right: F32
41	  {Elementwise.scalar(Elementwise.Add{}, left, right) == F32.add(left, right) : F32}
42	
43	law scalar_sub:
44	  for +left: F32
45	  for +right: F32
46	  {Elementwise.scalar(Elementwise.Sub{}, left, right) == F32.sub(left, right) : F32}
47	
48	law scalar_mul:
49	  for +left: F32
50	  for +right: F32
51	  {Elementwise.scalar(Elementwise.Mul{}, left, right) == F32.mul(left, right) : F32}
52	
53	law indexed_length:
54	  for +shape: Shape.Shape
55	  for tensor: Core.Tensor<shape>
56	  Core.LengthValid<shape, tensor>
57	
58	law successful_construction_dimensions:
59	  for +dimensions: List<&2, U32>
60	  for values: List<&2, F32>
61	  Core.ConstructionDimensions(dimensions, Core.construct(dimensions, values))
62	
63	law 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	
68	law 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	
74	law 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	
82	law 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	
88	law checked_dynamic_reader_source:
89	  for original: Core.Dynamic
90	  for +index: U32
91	  Core.DynamicSourceRead<original, index>
92	
93	law 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	
99	law checked_dynamic_reader_retains_source:
100	  for original: Core.Dynamic
101	  for +index: U32
102	  Core.DynamicSourceReadKeeps<original, index>
103	
104	law 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	
113	law 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	
118	law 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	
124	law storage_clone_first_length:
125	  for storage: Storage.Storage
126	  {Lifecycle.first_length(Storage.clone(storage)) == Lifecycle.logical_length(storage) : Nat}
127	
128	law storage_clone_second_length:
129	  for storage: Storage.Storage
130	  {Lifecycle.second_length(Storage.clone(storage)) == Lifecycle.logical_length(storage) : Nat}
131	
132	law 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	
140	law 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	
148	law 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	
163	law 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	
183	law 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	
193	law 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	
212	law 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	
218	law 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	
225	law 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	
231	law 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	
238	law 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	
245	law 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	
252	law 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	
261	law 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	
270	law 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	
278	law 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	
284	law 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	
293	law 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	
299	law 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	
305	law 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	
311	law 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>}