def reduce_to_fiber
bendtorch-core@0.1.0.0 · src/autograd/reduce_to_fold_PROOF.bend:212
import bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend as ReduceToFoldPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws
import bendtorch-core@0.1.0.0/src/autograd/reduce_fold_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend as Replay
212def reduce_to_fiber(+target: Shape.Shape, +shape: Shape.Shape, +plan: Shape.BroadcastPlan,
213 +planned: {Shape.broadcast_checked(target, shape) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>},
214 +same: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
215 +fill: F32, +ops: List<&2, StorageLaws.Op>,
216 -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
217 Laws.ReduceToContract<target, shape,
218 index => ReduceLaws.fiber(plan, Contracts.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))),
219 index, Shape.logical_numel(Shape.dimensions(shape))),
220 other => Replayed.value(shape, fill, ops, other),
221 Reduce.reduce_to(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, target)>:
222 +count = Shape.logical_numel(Shape.dimensions(shape))
223 Laws.ReduceToContract{
224 run_lift(target, shape, plan, planned, same, fill, ops, result => {ReduceLaws.succeeded(result) == True{} : Bool},
225 kept => values => words => kept_fits => out => cells => out_fits => {==})(fits),
226 run_lift(target, shape, plan, planned, same, fill, ops,
227 result => {Laws.output_dimensions(result) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>},
228 kept => values => words => kept_fits => out => cells => out_fits => {==})(fits),
229 index => inside =>
230 +inside = inside
231 run_lift(target, shape, plan, planned, same, fill, ops,
232 result => {Laws.output_point(result, index) ==
233 ReduceLaws.fiber(plan, Contracts.words(shape, fill, ops, count), index, count) : Maybe<&2, F32>},
234 kept => values => words => kept_fits => out => cells => out_fits =>
235 Equal.trans(Maybe<&2, F32>,
236 Core.dynamic_read_value(Core.read_dynamic(Core.Packed{target, Core.TTensor{Replayed.storage(target, 0.0, out), out_fits}}, index)),
237 Some{Replay.cell_word(plan, Shape.index_map(plan), shape, fill, ops, U32.to_nat(index))},
238 ReduceLaws.fiber(plan, Contracts.words(shape, fill, ops, count), index, count),
239 Equal.trans(Maybe<&2, F32>,
240 Core.dynamic_read_value(Core.read_dynamic(Core.Packed{target, Core.TTensor{Replayed.storage(target, 0.0, out), out_fits}}, index)),
241 Some{Replayed.value(target, 0.0, out, index)}, Some{Replay.cell_word(plan, Shape.index_map(plan), shape, fill, ops, U32.to_nat(index))},
242 PointwiseProof.replayed_point(target, 0.0, out, out_fits, index, inside),
243 Equal.cong(F32, Maybe<&2, F32>, word => Some{word}, Replayed.value(target, 0.0, out, index),
244 Replay.cell_word(plan, Shape.index_map(plan), shape, fill, ops, U32.to_nat(index)), cells(index)(inside))),
245 cell_fiber(target, shape, plan, planned, same, fill, ops, index, inside)))(fits),
246 other => inside =>
247 run_lift(target, shape, plan, planned, same, fill, ops,
248 result => {Laws.input_point(result, other) == Some{Replayed.value(shape, fill, ops, other)} : Maybe<&2, F32>},
249 kept => values => words => kept_fits => out => cells => out_fits =>
250 Equal.trans(Maybe<&2, F32>,
251 Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, kept), kept_fits}}, other)),
252 Some{Replayed.value(shape, fill, kept, other)}, Some{Replayed.value(shape, fill, ops, other)},
253 PointwiseProof.replayed_point(shape, fill, kept, kept_fits, other, inside),
254 Equal.cong(F32, Maybe<&2, F32>, word => Some{word}, Replayed.value(shape, fill, kept, other), Replayed.value(shape, fill, ops, other),
255 values(other))))(fits)}