1	import Base
2	import ../shape/core.bend as Shape
3	import ./core.bend as Core
4	import ./reduction.bend as Reduction
5	import ./math_totality.bend as Totality
6	
7	def LogicalValues(+fuel: Nat, -shape: Shape.Shape, -tensor: Core.Tensor<shape>, +cursor: Nat,
8	  values: List<&2, F32>) -> Data:
9	  match fuel values:
10	    case 0n Nil{}:
11	      Unit
12	    case 1n+tail value <> values:
13	      LogicalStep<tail, shape, tensor, cursor, value, values>
14	    case 0n value <> values:
15	      Empty
16	    case 1n+tail Nil{}:
17	      Empty
18	
19	type LogicalStep<-fuel: Nat, -shape: Shape.Shape, -tensor: Core.Tensor<shape>, -cursor: Nat,
20	  -value: F32, -values: List<&2, F32>> is Data:
21	  LogicalStep{-exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
22	    -observed: {Core.checked_observe(shape, tensor, U32.from_nat(cursor)) == Some{value} : Maybe<&2, F32>},
23	    -remaining: LogicalValues(fuel, shape, tensor, 1n+cursor, values)}
24	
25	type SumMeaning<-fuel: Nat, -shape: Shape.Shape, -tensor: Core.Tensor<shape>, -cursor: Nat,
26	  -accumulator: F32, -value: F32> is Data:
27	  SumMeaning{-values: List<&2, F32>, -logical: LogicalValues(fuel, shape, tensor, cursor, values),
28	    -fold: {value == Reduction.sequential_sum(values, accumulator) : F32}}
29	
30	def LoopMeaning(-fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -cursor: Nat, -accumulator: F32,
31	  result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>) -> Data:
32	  match result:
33	    case Fail{error}:
34	      Unit
35	    case Done{pair}:
36	      (tensor, value) = pair
37	      SumMeaning<fuel, shape, original, cursor, accumulator, value>
38	
39	type SourceSum<-fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -cursor: Nat, -accumulator: F32,
40	  -result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>> is Data:
41	  SourceSum{-meaning: @unit: Unit -> LoopMeaning(fuel, shape, original, cursor, accumulator, result)}
42	
43	law successful_loop_interpretation:
44	  for +fuel: Nat
45	  for -shape: Shape.Shape
46	  for tensor: Core.Tensor<shape>
47	  for +cursor: Nat
48	  for +accumulator: F32
49	  SourceSum<fuel, shape, tensor, cursor, accumulator, Reduction.natural_sum_loop(fuel, shape, tensor, cursor, accumulator)>
50	
51	def loop_value(-shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>) -> Maybe<&2, F32>:
52	  match result:
53	    case Fail{error}:
54	      None{}
55	    case Done{pair}:
56	      (tensor, value) = pair
57	      Some{value}
58	
59	def retained_observe(-shape: Shape.Shape, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>, +other: U32) -> Maybe<&2, F32>:
60	  match result:
61	    case Fail{error}:
62	      None{}
63	    case Done{pair}:
64	      (tensor, value) = pair
65	      Core.checked_observe(shape, tensor, other)
66	
67	def successful_observe(-shape: Shape.Shape, original: Core.Tensor<shape>,
68	  result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>, +other: U32) -> Maybe<&2, F32>:
69	  match result:
70	    case Fail{error}:
71	      None{}
72	    case Done{pair}:
73	      Core.checked_observe(shape, original, other)
74	
75	type Preserved<-shape: Shape.Shape, -original: Core.Tensor<shape>,
76	  -result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>> is Data:
77	  Preserved{-kept: @+other: U32 ->
78	    {retained_observe(shape, result, other) == successful_observe(shape, original, result, other) : Maybe<&2, F32>}}
79	
80	type Interpretation<-actual: Maybe<&2, F32>, -expected: Maybe<&2, F32>> is Data:
81	  Interpretation{-proof: @unit: Unit -> {actual == expected : Maybe<&2, F32>}}
82	
83	law ordered_loop_interpretation:
84	  for +fuel: Nat
85	  for -shape: Shape.Shape
86	  for tensor: Core.Tensor<shape>
87	  for +cursor: Nat
88	  for +accumulator: F32
89	  for +values: List<&2, F32>
90	  for logical: LogicalValues(fuel, shape, tensor, cursor, values)
91	  Interpretation<loop_value(shape, Reduction.natural_sum_loop(fuel, shape, tensor, cursor, accumulator)),
92	    Some{Reduction.sequential_sum(values, accumulator)}>
93	
94	law ordered_loop_preservation:
95	  for +fuel: Nat
96	  for -shape: Shape.Shape
97	  for tensor: Core.Tensor<shape>
98	  for +cursor: Nat
99	  for +accumulator: F32
100	  Preserved<shape, tensor, Reduction.natural_sum_loop(fuel, shape, tensor, cursor, accumulator)>
101	
102	law ordered_sum_interpretation:
103	  for +shape: Shape.Shape
104	  for tensor: Core.Tensor<shape>
105	  for +values: List<&2, F32>
106	  for logical: LogicalValues(Shape.logical_numel(Shape.dimensions(shape)), shape, tensor, 0n, values)
107	  Interpretation<Reduction.sum_observation(shape, Reduction.sum(shape, tensor)), Some{Reduction.sequential_sum(values, 0.0)}>
108	
109	type SumResult<-shape: Shape.Shape, -original: Core.Tensor<shape>, -retained: Core.Tensor<shape>,
110	  -scalar: Core.Tensor<Reduction.scalar_shape()>> is Data:
111	  SumResult{-values: List<&2, F32>, -logical: LogicalValues(Shape.logical_numel(Shape.dimensions(shape)), shape, original, 0n, values),
112	    -meaning: {Core.observe(Reduction.scalar_shape(), scalar, 0) == Some{Reduction.sequential_sum(values, 0.0)} : Maybe<&2, F32>},
113	    -kept: @+index: U32 -> {Core.checked_observe(shape, retained, index) == Core.checked_observe(shape, original, index) : Maybe<&2, F32>}}
114	
115	def SumResultMeaning(-shape: Shape.Shape, -original: Core.Tensor<shape>,
116	  result: Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>) -> Data:
117	  match result:
118	    case Fail{error}:
119	      Unit
120	    case Done{pair}:
121	      (retained, scalar) = pair
122	      SumResult<shape, original, retained, scalar>
123	
124	type SourceSumResult<-shape: Shape.Shape, -original: Core.Tensor<shape>,
125	  -result: Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>> is Data:
126	  SourceSumResult{-meaning: @unit: Unit -> SumResultMeaning(shape, original, result)}
127	
128	law successful_sum_interpretation:
129	  for +shape: Shape.Shape
130	  for tensor: Core.Tensor<shape>
131	  SourceSumResult<shape, tensor, Reduction.sum(shape, tensor)>
132	
133	type DynamicSumSuccess<-original: Core.Dynamic, -retained: Core.Dynamic, -scalar: Core.Dynamic> is Data:
134	  DynamicSumSuccess{-shape: Shape.Shape, -input: Core.Tensor<shape>, -owner: Core.Tensor<shape>, -output: Core.Tensor<Reduction.scalar_shape()>,
135	    -input_exact: {original == Core.Packed{shape, input} : Core.Dynamic}, -owner_exact: {retained == Core.Packed{shape, owner} : Core.Dynamic},
136	    -scalar_exact: {scalar == Core.Packed{Reduction.scalar_shape(), output} : Core.Dynamic}, -source: SumResult<shape, input, owner, output>}
137	
138	def DynamicSumMeaning(-original: Core.Dynamic, result: Result<&2, &1, Core.Error, Core.Dynamic & Core.Dynamic>) -> Data:
139	  match result:
140	    case Fail{error}:
141	      Unit
142	    case Done{pair}:
143	      (retained, scalar) = pair
144	      DynamicSumSuccess<original, retained, scalar>
145	
146	type SourceDynamicSum<-original: Core.Dynamic, -result: Result<&2, &1, Core.Error, Core.Dynamic & Core.Dynamic>> is Data:
147	  SourceDynamicSum{-meaning: @unit: Unit -> DynamicSumMeaning(original, result)}
148	
149	law successful_dynamic_sum_interpretation:
150	  for tensor: Core.Dynamic
151	  SourceDynamicSum<tensor, Reduction.sum_dynamic(tensor)>
152	
153	law empty_accumulation:
154	  for -shape: Shape.Shape
155	  for tensor: Core.Tensor<shape>
156	  for +index: U32
157	  for accumulator: F32
158	  {Reduction.sum_loop(0n, shape, tensor, index, accumulator) == Done{(tensor, accumulator)} : Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>}
159	
160	law empty_sum_identity:
161	  for +shape: Shape.Shape
162	  for tensor: Core.Tensor<shape>
163	  for empty: {Shape.logical_numel(Shape.dimensions(shape)) == 0n : Nat}
164	  {Reduction.sum_observation(shape, Reduction.sum(shape, tensor)) == Some{0.0} : Maybe<&2, F32>}
165	
166	law sum_valid_success:
167	  for +shape: Shape.Shape
168	  for tensor: Core.Tensor<shape>
169	  Totality.Success<Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, Reduction.sum(shape, tensor)>
170	
171	law sum_dynamic_valid_success:
172	  for tensor: Core.Dynamic
173	  Totality.Success<Core.Error, Core.Dynamic & Core.Dynamic, Reduction.sum_dynamic(tensor)>
174	
175	type TotalSum<-shape: Shape.Shape, -original: Core.Tensor<shape>,
176	  -result: Result<&2, &1, Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>>> is Data:
177	  TotalSum{-done: Totality.Success<Core.Error, Core.Tensor<shape> & Core.Tensor<Reduction.scalar_shape()>, result>,
178	    -interpretation: SourceSumResult<shape, original, result>}
179	
180	type TotalDynamicSum<-original: Core.Dynamic, -result: Result<&2, &1, Core.Error, Core.Dynamic & Core.Dynamic>> is Data:
181	  TotalDynamicSum{-done: Totality.Success<Core.Error, Core.Dynamic & Core.Dynamic, result>,
182	    -interpretation: SourceDynamicSum<original, result>}
183	
184	law sum_valid_result:
185	  for +shape: Shape.Shape
186	  for tensor: Core.Tensor<shape>
187	  TotalSum<shape, tensor, Reduction.sum(shape, tensor)>
188	
189	law sum_dynamic_valid_result:
190	  for tensor: Core.Dynamic
191	  TotalDynamicSum<tensor, Reduction.sum_dynamic(tensor)>