src/tensor/reshape_contract.bend
bendtorch-core@0.1.0.0 · 239 lines · 22 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
4import bendtorch-core@0.1.0.0/src/shape/PROOF.bend as ShapeProof
5import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
6import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
7import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
8import bendtorch-core@0.1.0.0/src/storage/PROOF.bend as StorageProof
9import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
10import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
11import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
12import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
13import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose
14import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
15import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof
16import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
17import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
18import bendtorch-core@0.1.0.0/src/tensor/transform_observation.bend as Observation
19import bendtorch-core@0.1.0.0/src/tensor/transform_records.bend as Laws
20import bendtorch-core@0.1.0.0/src/tensor/write_contract.bend as Writes
21
22def shape_complete(+shape: Shape.Shape) ->
23 {ShapeLaws.built(Shape.dimensions(shape), Shape.construct(Shape.dimensions(shape))) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
24 match shape:
25 case Shape.SShape{+dimensions, size, exact, rank_bound, capacity_bound}:
26 ShapeLaws.construction_complete(dimensions, rank_bound, capacity_bound)
27
28def inside_input(+input: Shape.Shape, +target: Shape.Shape, +other: U32, same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}:
29 %Equal.sym(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)), same) : {Nat.is_lt(U32.to_nat(other), _) == True{} : Bool}
30 inside
31
32def elements_output(+input: Shape.Shape, +target: Shape.Shape, +output: Shape.Shape, same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat},
33 preserved: {Shape.dimensions(output) == Shape.dimensions(target) : List<&2, U32>}) ->
34 {Shape.elements(input) == Shape.elements(output) : Nat}:
35 Equal.trans(Nat, Shape.elements(input), Shape.logical_numel(Shape.dimensions(input)), Shape.elements(output), Shape.elements_exact(input),
36 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)), Shape.elements(output), same,
37 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(target)), Shape.logical_numel(Shape.dimensions(output)), Shape.elements(output),
38 Equal.cong(List<&2, U32>, Nat, dims => Shape.logical_numel(dims), Shape.dimensions(target), Shape.dimensions(output),
39 Equal.sym(List<&2, U32>, Shape.dimensions(output), Shape.dimensions(target), preserved)),
40 Equal.sym(Nat, Shape.elements(output), Shape.logical_numel(Shape.dimensions(output)), Shape.elements_exact(output)))))
41
42def decided_lift(+input: Shape.Shape, +output: Shape.Shape, -storage: Storage.Storage,
43 -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(input)) : Nat},
44 decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(output))>,
45 counted: {Shape.elements(input) == Shape.elements(output) : Nat},
46 -P: Result<&2, &1, Transforms.Error, Core.Dynamic> -> Type,
47 h: @-fits: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(output)) : Nat} -> P(Done{Core.Packed{output, Core.TTensor{storage, fits}}})) ->
48 P(Transforms.reshape_decided(input, output, Core.TTensor{storage, valid}, decision)):
49 match decision:
50 case Shape.BFalse{no}:
51 Empty.absurd(P(Transforms.reshape_decided(input, output, Core.TTensor{storage, valid}, Shape.BFalse{no})),
52 Nats.contradiction(Nat.is_eq(Shape.elements(input), Shape.elements(output)),
53 AllocationProof.natural_equal_true(Shape.elements(input), Shape.elements(output), counted), no))
54 case Shape.BTrue{yes}:
55 h(Equal.trans(Nat, Lifecycle.logical_length(storage), Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(output)), valid, Transforms.elements_equal(input, output, yes)))
56
57def built_lift(+input: Shape.Shape, +target: Shape.Shape, -storage: Storage.Storage,
58 -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(input)) : Nat},
59 built: Shape.ConstructResult<Shape.dimensions(target)>,
60 complete: {ShapeLaws.built(Shape.dimensions(target), built) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
61 +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}, -P: Result<&2, &1, Transforms.Error, Core.Dynamic> -> Type,
62 h: @+output: Shape.Shape -> @preserved: {Shape.dimensions(output) == Shape.dimensions(target) : List<&2, U32>} ->
63 @-fits: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(output)) : Nat} -> P(Done{Core.Packed{output, Core.TTensor{storage, fits}}})) ->
64 P(Transforms.reshape_built(input, Core.TTensor{storage, valid}, Shape.dimensions(target), built)):
65 match built:
66 case Shape.SError{error}:
67 Empty.absurd(P(Transforms.reshape_built(input, Core.TTensor{storage, valid}, Shape.dimensions(target), Shape.SError{error})),
68 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, found => Maybe.is_some(&2, List<&2, U32>, found), None{}, Some{Shape.dimensions(target)}, complete)))
69 case Shape.SBuilt{+output, +preserved}:
70 decided_lift(input, output, storage, valid, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))),
71 elements_output(input, target, output, same, preserved), P, h(output, preserved))
72
73def reshape_lift(+input: Shape.Shape, +target: Shape.Shape, -storage: Storage.Storage,
74 -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}, -P: Result<&2, &1, Transforms.Error, Core.Dynamic> -> Type,
75 h: @+output: Shape.Shape -> @preserved: {Shape.dimensions(output) == Shape.dimensions(target) : List<&2, U32>} ->
76 @-fits: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(output)) : Nat} -> P(Done{Core.Packed{output, Core.TTensor{storage, fits}}})) ->
77 P(Transforms.reshape(input, Core.TTensor{storage, valid}, Shape.dimensions(target))):
78 built_lift(input, target, storage, valid, Shape.construct(Shape.dimensions(target)), shape_complete(target), same, P, h)
79
80def dynamic_value(+output: Shape.Shape, -storage: Storage.Storage,
81 -fits: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(output)) : Nat}, +other: U32,
82 pair: Storage.Storage & Result<&2, &2, Storage.Error, F32>, -equal: {pair == Storage.get(storage, other) : Storage.Storage & Result<&2, &2, Storage.Error, F32>}) ->
83 {Core.dynamic_read_value(Core.read_dynamic_result(output, Core.read_result(output, storage, fits, other, pair, equal))) ==
84 Lifecycle.read_value(pair) : Maybe<&2, F32>}:
85 (kept, result) = pair
86 match result:
87 case Fail{error}:
88 {==}
89 case Done{value}:
90 {==}
91
92def reshaped_value(+input: Shape.Shape, +target: Shape.Shape, storage: Storage.Storage,
93 -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +other: U32, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) ->
94 {Observation.output_value(other, Transforms.reshape(input, Core.TTensor{storage, valid}, Shape.dimensions(target))) ==
95 Lifecycle.read_value(Storage.get(storage, other)) : Maybe<&2, F32>}:
96 reshape_lift(input, target, storage, valid, same,
97 result => {Observation.output_value(other, result) == Lifecycle.read_value(Storage.get(storage, other)) : Maybe<&2, F32>},
98 output => preserved => fits => dynamic_value(output, storage, fits, other, Storage.get(storage, other), {==}))
99
100def reshape_outcome(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) ->
101 {Observation.reshape_code(input, Shape.dimensions(target), Core.new(input, fill)) == Some{0} : Maybe<&2, U32>}:
102 Reads.new_lift(input, fill, result => {Observation.reshape_code(input, Shape.dimensions(target), result) == Some{0} : Maybe<&2, U32>},
103 valid => reshape_lift(input, target, StorageLaws.created(Shape.count(input), fill), valid, same,
104 result => {Some{Observation.status(result)} == Some{0} : Maybe<&2, U32>},
105 output => preserved => fits => {==}))
106
107def reshape_dimensions(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) ->
108 {Observation.reshape_dimensions(input, Shape.dimensions(target), Core.new(input, fill)) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>}:
109 Reads.new_lift(input, fill, result => {Observation.reshape_dimensions(input, Shape.dimensions(target), result) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
110 valid => reshape_lift(input, target, StorageLaws.created(Shape.count(input), fill), valid, same,
111 result => {Observation.output_dimensions(result) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
112 output => preserved => fits => Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, dims => Some{dims}, Shape.dimensions(output), Shape.dimensions(target), preserved)))
113
114def reshape_length(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) ->
115 {Observation.reshape_length(input, Shape.dimensions(target), Core.new(input, fill)) == Some{Shape.logical_numel(Shape.dimensions(target))} : Maybe<&2, Nat>}:
116 Reads.new_lift(input, fill, result => {Observation.reshape_length(input, Shape.dimensions(target), result) == Some{Shape.logical_numel(Shape.dimensions(target))} : Maybe<&2, Nat>},
117 valid => reshape_lift(input, target, StorageLaws.created(Shape.count(input), fill), valid, same,
118 result => {Observation.output_length(result) == Some{Shape.logical_numel(Shape.dimensions(target))} : Maybe<&2, Nat>},
119 output => preserved => fits => Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)), Shape.logical_numel(Shape.dimensions(target)),
120 Equal.trans(Nat, Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)), Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)), Reads.created_exact(input, fill), same))))
121
122def reshape_count(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) ->
123 {Observation.reshape_count(input, Shape.dimensions(target), Core.new(input, fill)) == Some{Shape.count(target)} : Maybe<&2, U32>}:
124 Reads.new_lift(input, fill, result => {Observation.reshape_count(input, Shape.dimensions(target), result) == Some{Shape.count(target)} : Maybe<&2, U32>},
125 valid => reshape_lift(input, target, StorageLaws.created(Shape.count(input), fill), valid, same,
126 result => {Observation.output_count(result) == Some{Shape.count(target)} : Maybe<&2, U32>},
127 output => preserved => fits => Equal.cong(Nat, Maybe<&2, U32>, number => Some{U32.from_nat(number)}, Shape.elements(output), Shape.elements(target),
128 Equal.trans(Nat, Shape.elements(output), Shape.elements(input), Shape.elements(target),
129 Equal.sym(Nat, Shape.elements(input), Shape.elements(output), elements_output(input, target, output, same, preserved)),
130 Equal.trans(Nat, Shape.elements(input), Shape.logical_numel(Shape.dimensions(input)), Shape.elements(target), Shape.elements_exact(input),
131 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)), Shape.elements(target), same, Equal.sym(Nat, Shape.elements(target), Shape.logical_numel(Shape.dimensions(target)), Shape.elements_exact(target))))))))
132
133def reshape_value_done(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +other: U32, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}) ->
134 {Observation.reshape_value(input, Shape.dimensions(target), other, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
135 Equal.trans(Maybe<&2, F32>, Observation.output_value(other, Transforms.reshape(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Shape.dimensions(target))),
136 Lifecycle.read_value(Storage.get(StorageLaws.created(Shape.count(input), fill), other)), Some{fill},
137 reshaped_value(input, target, StorageLaws.created(Shape.count(input), fill), valid, other, same),
138 Reads.stored_value(StorageLaws.created(Shape.count(input), fill), other, fill,
139 StorageLaws.replay_get(Shape.count(input), fill, [], other, Conversion.shape_count_within(input),
140 Reads.word_inside(input, other, inside_input(input, target, other, same, inside)))))
141
142def written_projection(+input: Shape.Shape, +target: Shape.Shape, -original: Storage.Storage,
143 -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +index: U32, +value: F32, +other: U32, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat},
144 pair: Storage.Storage & Result<&2, &2, Storage.Error, Unit>,
145 -equal: {pair == Storage.set(original, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
146 {Observation.reshape_written_pair(input, Shape.dimensions(target), other, Core.write_result(input, original, valid, index, value, pair, equal)) ==
147 Lifecycle.read_value(Storage.get(StorageLaws.owner(Result<&2, &2, Storage.Error, Unit>, pair), other)) : Maybe<&2, F32>}:
148 (storage, result) = pair
149 reshaped_value(input, target, storage,
150 Equal.trans(Nat, Lifecycle.logical_length(storage), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(input)),
151 %Equal.sym(Storage.Storage & Result<&2, &2, Storage.Error, Unit>, (storage, result), Storage.set(original, index, value), equal) :
152 {Lifecycle.retained_write(_) == Lifecycle.logical_length(original) : Nat}
153 Lifecycle.set_length(original, index, value), valid),
154 other, same)
155
156def written_done(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(input), fill)) == Shape.logical_numel(Shape.dimensions(input)) : Nat}, +index: U32, +value: F32, +other: U32, +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}) ->
157 {Observation.reshape_written(input, index, value, Shape.dimensions(target), other, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}) ==
158 Some{Writes.written_pick(input, index, value, other, fill)} : Maybe<&2, F32>}:
159 Equal.trans(Maybe<&2, F32>,
160 Observation.reshape_written_pair(input, Shape.dimensions(target), other,
161 Core.write_result(input, StorageLaws.created(Shape.count(input), fill), valid, index, value, Storage.set(StorageLaws.created(Shape.count(input), fill), index, value), {==})),
162 Lifecycle.read_value(Storage.get(StorageLaws.written(StorageLaws.created(Shape.count(input), fill), index, value), other)),
163 Some{Writes.written_pick(input, index, value, other, fill)},
164 written_projection(input, target, StorageLaws.created(Shape.count(input), fill), valid, index, value, other, same, Storage.set(StorageLaws.created(Shape.count(input), fill), index, value), {==}),
165 Reads.stored_value(StorageLaws.written(StorageLaws.created(Shape.count(input), fill), index, value), other, Writes.written_pick(input, index, value, other, fill),
166 StorageLaws.replay_get(Shape.count(input), fill, [StorageLaws.Write{index, value}], other, Conversion.shape_count_within(input),
167 Reads.word_inside(input, other, inside_input(input, target, other, same, inside)))))
168
169def reshape_written(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, +index: U32, +value: F32, +other: U32, -expected: F32,
170 +same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}, picked: {Writes.written_pick(input, index, value, other, fill) == expected : F32}) ->
171 {Observation.reshape_written(input, index, value, Shape.dimensions(target), other, Core.new(input, fill)) == Some{expected} : Maybe<&2, F32>}:
172 Reads.new_lift(input, fill, result => {Observation.reshape_written(input, index, value, Shape.dimensions(target), other, result) == Some{expected} : Maybe<&2, F32>},
173 valid => Equal.trans(Maybe<&2, F32>, Observation.reshape_written(input, index, value, Shape.dimensions(target), other, Done{Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}}),
174 Some{Writes.written_pick(input, index, value, other, fill)}, Some{expected},
175 written_done(input, fill, target, valid, index, value, other, same, inside),
176 Equal.cong(F32, Maybe<&2, F32>, number => Some{number}, Writes.written_pick(input, index, value, other, fill), expected, picked)))
177
178def target_inside(+input: Shape.Shape, +target: Shape.Shape, +index: U32, same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat},
179 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}:
180 %same : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
181 inside
182
183def reshape_contract(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) -> Laws.ReshapeContract<input, fill, target>:
184 +same = same
185 Laws.ReshapeContract{
186 reshape_outcome(input, fill, target, same),
187 reshape_dimensions(input, fill, target, same),
188 reshape_length(input, fill, target, same),
189 reshape_count(input, fill, target, same),
190 other => inside => Reads.new_lift(input, fill, result => {Observation.reshape_value(input, Shape.dimensions(target), other, result) == Some{fill} : Maybe<&2, F32>},
191 valid => reshape_value_done(input, fill, target, valid, other, same, inside))}
192
193def reshape_write(+input: Shape.Shape, +fill: F32, +target: Shape.Shape, +index: U32, +value: F32,
194 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}, same: {Shape.logical_numel(Shape.dimensions(input)) == Shape.logical_numel(Shape.dimensions(target)) : Nat}) -> Laws.ReshapeWrite<input, fill, target, index, value>:
195 +inside = inside
196 +same = same
197 Laws.ReshapeWrite{
198 reshape_written(input, fill, target, index, value, index, value, same, target_inside(input, target, index, same, inside),
199 Writes.pick_hit(input, index, value, fill, inside)),
200 other => inside_other => different =>
201 reshape_written(input, fill, target, index, value, other, fill, same, inside_other,
202 Writes.pick_frame(input, index, value, other, fill, inside, different))}
203
204def mismatch_decided(+input: Shape.Shape, +target: Shape.Shape, +output: Shape.Shape, -tensor: Core.Tensor<input>,
205 decision: Shape.BoolCase<Nat.is_eq(Shape.elements(input), Shape.elements(output))>,
206 preserved: {Shape.dimensions(output) == Shape.dimensions(target) : List<&2, U32>},
207 different: {Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))) == False{} : Bool}) ->
208 {Transforms.reshape_decided(input, output, tensor, decision) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} : Result<&2, &1, Transforms.Error, Core.Dynamic>}:
209 match decision:
210 case Shape.BFalse{no}:
211 {==}
212 case Shape.BTrue{yes}:
213 Empty.absurd({Transforms.reshape_decided(input, output, tensor, Shape.BTrue{yes}) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} : Result<&2, &1, Transforms.Error, Core.Dynamic>},
214 Nats.contradiction(Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))),
215 AllocationProof.natural_equal_true(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target)),
216 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(output)), Shape.logical_numel(Shape.dimensions(target)), Transforms.elements_equal(input, output, yes),
217 Equal.cong(List<&2, U32>, Nat, dims => Shape.logical_numel(dims), Shape.dimensions(output), Shape.dimensions(target), preserved))),
218 Equal.sym(Bool, Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))), False{}, different)))
219
220def mismatch_built(+input: Shape.Shape, +target: Shape.Shape, -tensor: Core.Tensor<input>,
221 built: Shape.ConstructResult<Shape.dimensions(target)>,
222 complete: {ShapeLaws.built(Shape.dimensions(target), built) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
223 different: {Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))) == False{} : Bool}) ->
224 {Transforms.reshape_built(input, tensor, Shape.dimensions(target), built) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} : Result<&2, &1, Transforms.Error, Core.Dynamic>}:
225 match built:
226 case Shape.SError{error}:
227 Empty.absurd({Transforms.reshape_built(input, tensor, Shape.dimensions(target), Shape.SError{error}) == Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}} : Result<&2, &1, Transforms.Error, Core.Dynamic>},
228 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, found => Maybe.is_some(&2, List<&2, U32>, found), None{}, Some{Shape.dimensions(target)}, complete)))
229 case Shape.SBuilt{+output, preserved}:
230 mismatch_decided(input, target, output, tensor, Shape.bool_case(Nat.is_eq(Shape.elements(input), Shape.elements(output))), preserved, different)
231
232def reshape_count_mismatch(+input: Shape.Shape, +fill: F32, +target: Shape.Shape,
233 different: {Nat.is_eq(Shape.logical_numel(Shape.dimensions(input)), Shape.logical_numel(Shape.dimensions(target))) == False{} : Bool}) ->
234 {Observation.reshape_code(input, Shape.dimensions(target), Core.new(input, fill)) == Some{15} : Maybe<&2, U32>}:
235 +different = different
236 Reads.new_lift(input, fill, result => {Observation.reshape_code(input, Shape.dimensions(target), result) == Some{15} : Maybe<&2, U32>},
237 valid => Equal.cong(Result<&2, &1, Transforms.Error, Core.Dynamic>, Maybe<&2, U32>, result => Some{Observation.status(result)},
238 Transforms.reshape(input, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Shape.dimensions(target)), Fail{Transforms.LayoutError{Layout.ElementCountMismatch{}}},
239 mismatch_built(input, target, Core.TTensor{StorageLaws.created(Shape.count(input), fill), valid}, Shape.construct(Shape.dimensions(target)), shape_complete(target), different)))