BroadcastPointwisePROOF.run_lift: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_PROOF.bend as BroadcastPointwisePROOF Lines 109-137 of bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_PROOF.bend&start_line=109&end_line=137 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/layout.bend as Layout import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_LAWS.bend as BinaryLaws import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend as Binary import bendtorch-core@0.1.0.0/src/autograd/broadcast.bend as Broadcast import bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend as ReduceTo import bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_LAWS.bend as Laws # broadcast_to on a replayed input whose shape broadcasts to exactly the # target: the planner and the target check pass, the zero tensor of the target # is allocated, and the parallel build runs KeepLeft with the input on the # left and the zero tensor on the right, whose words are `cells`. def run_lift(+shape: Shape.Shape, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +planned: {Shape.broadcast_checked(shape, target) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, +same: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(target) : List<&2, U32>}, +fill: F32, +ops: List<&2, StorageLaws.Op>, -P: Core.Dynamic & Result<&2, &1, Broadcast.Error, Core.Dynamic> -> Type, h: Laws.BroadcastWith(plan, shape, fill, ops, P)) -> @-fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} -> P(Broadcast.broadcast_to(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, target)): +output = Shape.output_shape(plan) +count = Shape.logical_numel(Shape.dimensions(output)) fits => -input = {Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}} : Core.Dynamic} %Equal.sym(Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, Shape.broadcast_checked(shape, target), Done{plan}, planned) : P(Broadcast.planned(input, target, _)) %Equal.sym(Bool, Layout.words_same(Shape.dimensions(output), Shape.dimensions(target)), True{}, ReduceTo.fitted_same(target, plan, same)) : P(Broadcast.fitted(input, target, plan, _)) Replayed.new_lift(target, 0.0, result => P(Broadcast.zeroed(input, target, plan, result)), zeros_fits => Binary.allocated_replayed(Elementwise.KeepLeft{}, plan, shape, fill, ops, target, 0.0, Nil{}, planned, pair => P(Broadcast.finish(pair)), kept => kept_words => input_fits => zeros_kept => zeros_words => zeros_kept_fits => output_ops => values => output_fits => h(kept, kept_words, input_fits, output_ops, Equal.trans(List<&2, F32>, Contracts.words(output, 0.0, output_ops, count), BinaryLaws.cells(Elementwise.KeepLeft{}, plan, shape, fill, ops, target, 0.0, Nil{}, count), Laws.cells(plan, shape, fill, ops, count), values, cells_keep(plan, shape, fill, ops, target, count)), output_fits))(fits, zeros_fits)) Uses (37): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym 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=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair 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=bendtorch-core@0.1.0.0/src/autograd/broadcast.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast.bend&name=broadcast_to https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast.bend&name=finish https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast.bend&name=fitted https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast.bend&name=planned https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast.bend&name=zeroed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_LAWS.bend&name=BroadcastWith https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_LAWS.bend&name=cells https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_PROOF.bend&name=cells_keep https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend&name=fitted_same 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=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/binary_LAWS.bend&name=cells https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&name=allocated_replayed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=new_lift 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/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/elementwise.bend&name=Operation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=words_same https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=logical_length