BroadcastPointwisePROOF.broadcast_to_pointwise: 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 147-190 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=147&end_line=190 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/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/pointwise_proof.bend as PointwiseProof import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend as PointwiseBroadcast import bendtorch-core@0.1.0.0/src/autograd/broadcast.bend as Broadcast import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws import bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_LAWS.bend as Laws def broadcast_to_pointwise(+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>, -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) -> Laws.BroadcastToContract Replayed.value(shape, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, index))), other => Replayed.value(shape, fill, ops, other), 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)) +total = Shape.logical_numel(Shape.dimensions(shape)) run_lift(shape, target, plan, planned, same, fill, ops, result => Laws.BroadcastToContract Replayed.value(shape, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, index))), other => Replayed.value(shape, fill, ops, other), result>, kept => kept_words => input_fits => output_ops => values => output_fits => Laws.BroadcastToContract{ {==}, Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, dimensions => Some{dimensions}, Shape.dimensions(output), Shape.dimensions(target), same), index => inside => +below = output_below(plan, target, index, same, inside) Equal.trans(Maybe<&2, F32>, Core.dynamic_read_value(Core.read_dynamic(Core.Packed{output, Core.TTensor{Replayed.storage(output, 0.0, output_ops), output_fits}}, index)), Some{Replayed.value(output, 0.0, output_ops, index)}, Some{Replayed.value(shape, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, U32.to_nat(index))))}, PointwiseProof.replayed_point(output, 0.0, output_ops, output_fits, index, below), Equal.trans(Maybe<&2, F32>, Some{Replayed.value(output, 0.0, output_ops, index)}, ReduceLaws.word_at(Laws.cells(plan, shape, fill, ops, count), U32.to_nat(index)), Some{Replayed.value(shape, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, U32.to_nat(index))))}, listed_value(output, 0.0, output_ops, count, Laws.cells(plan, shape, fill, ops, count), index, values, below), cells_at(plan, shape, fill, ops, count, U32.to_nat(index), below))), other => inside => +within = {inside : {Nat.is_lt(U32.to_nat(other), total) == True{} : Bool}} Equal.trans(Maybe<&2, F32>, Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, kept), input_fits}}, other)), Some{Replayed.value(shape, fill, kept, other)}, Some{Replayed.value(shape, fill, ops, other)}, PointwiseProof.replayed_point(shape, fill, kept, input_fits, other, within), Equal.trans(Maybe<&2, F32>, Some{Replayed.value(shape, fill, kept, other)}, ReduceLaws.word_at(Contracts.words(shape, fill, ops, total), U32.to_nat(other)), Some{Replayed.value(shape, fill, ops, other)}, listed_value(shape, fill, kept, total, Contracts.words(shape, fill, ops, total), other, kept_words, within), Equal.sym(Maybe<&2, F32>, Some{Replayed.value(shape, fill, ops, other)}, ReduceLaws.word_at(Contracts.words(shape, fill, ops, total), U32.to_nat(other)), listed_value(shape, fill, ops, total, Contracts.words(shape, fill, ops, total), other, {==}, within))))})(fits) Uses (39): 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.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=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt 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.from_nat 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/broadcast.bend&name=broadcast_to https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_LAWS.bend&name=BroadcastToContract 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_at https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_PROOF.bend&name=listed_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_PROOF.bend&name=output_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_PROOF.bend&name=run_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=word_at 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/broadcast.bend&name=left_map 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