ReduceToFoldPROOF.reduce_to_fiber: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend as ReduceToFoldPROOF Lines 212-255 of bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend&start_line=212&end_line=255 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 def reduce_to_fiber(+target: Shape.Shape, +shape: Shape.Shape, +plan: Shape.BroadcastPlan, +planned: {Shape.broadcast_checked(target, shape) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, +same: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>}, +fill: F32, +ops: List<&2, StorageLaws.Op>, -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) -> Laws.ReduceToContract ReduceLaws.fiber(plan, Contracts.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))), index, Shape.logical_numel(Shape.dimensions(shape))), other => Replayed.value(shape, fill, ops, other), Reduce.reduce_to(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, target)>: +count = Shape.logical_numel(Shape.dimensions(shape)) Laws.ReduceToContract{ run_lift(target, shape, plan, planned, same, fill, ops, result => {ReduceLaws.succeeded(result) == True{} : Bool}, kept => values => words => kept_fits => out => cells => out_fits => {==})(fits), run_lift(target, shape, plan, planned, same, fill, ops, result => {Laws.output_dimensions(result) == Some{Shape.dimensions(target)} : Maybe<&2, List<&2, U32>>}, kept => values => words => kept_fits => out => cells => out_fits => {==})(fits), index => inside => +inside = inside run_lift(target, shape, plan, planned, same, fill, ops, result => {Laws.output_point(result, index) == ReduceLaws.fiber(plan, Contracts.words(shape, fill, ops, count), index, count) : Maybe<&2, F32>}, kept => values => words => kept_fits => out => cells => out_fits => Equal.trans(Maybe<&2, F32>, Core.dynamic_read_value(Core.read_dynamic(Core.Packed{target, Core.TTensor{Replayed.storage(target, 0.0, out), out_fits}}, index)), Some{Replay.cell_word(plan, Shape.index_map(plan), shape, fill, ops, U32.to_nat(index))}, ReduceLaws.fiber(plan, Contracts.words(shape, fill, ops, count), index, count), Equal.trans(Maybe<&2, F32>, Core.dynamic_read_value(Core.read_dynamic(Core.Packed{target, Core.TTensor{Replayed.storage(target, 0.0, out), out_fits}}, index)), Some{Replayed.value(target, 0.0, out, index)}, Some{Replay.cell_word(plan, Shape.index_map(plan), shape, fill, ops, U32.to_nat(index))}, PointwiseProof.replayed_point(target, 0.0, out, out_fits, index, inside), Equal.cong(F32, Maybe<&2, F32>, word => Some{word}, Replayed.value(target, 0.0, out, index), Replay.cell_word(plan, Shape.index_map(plan), shape, fill, ops, U32.to_nat(index)), cells(index)(inside))), cell_fiber(target, shape, plan, planned, same, fill, ops, index, inside)))(fits), other => inside => run_lift(target, shape, plan, planned, same, fill, ops, result => {Laws.input_point(result, other) == Some{Replayed.value(shape, fill, ops, other)} : Maybe<&2, F32>}, kept => values => words => kept_fits => out => cells => out_fits => Equal.trans(Maybe<&2, F32>, Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, kept), kept_fits}}, other)), Some{Replayed.value(shape, fill, kept, other)}, Some{Replayed.value(shape, fill, ops, other)}, PointwiseProof.replayed_point(shape, fill, kept, kept_fits, other, inside), Equal.cong(F32, Maybe<&2, F32>, word => Some{word}, Replayed.value(shape, fill, kept, other), Replayed.value(shape, fill, ops, other), values(other))))(fits)} Uses (38): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=reduce_to https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=fiber https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=succeeded https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold_LAWS.bend&name=ReduceToContract https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold_LAWS.bend&name=input_point https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold_LAWS.bend&name=output_dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold_LAWS.bend&name=output_point https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=cell_word https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend&name=cell_fiber https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend&name=run_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_checked https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_map https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&name=words https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend&name=replayed_point https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=storage https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=dynamic_read_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=logical_length