def broadcast_to_pointwise
bendtorch-core@0.1.0.0 · src/autograd/broadcast_pointwise_PROOF.bend:147
import bendtorch-core@0.1.0.0/src/autograd/broadcast_pointwise_PROOF.bend as BroadcastPointwisePROOF
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
147def broadcast_to_pointwise(+shape: Shape.Shape, +target: Shape.Shape, +plan: Shape.BroadcastPlan,
148 +planned: {Shape.broadcast_checked(shape, target) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>},
149 +same: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
150 +fill: F32, +ops: List<&2, StorageLaws.Op>,
151 -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
152 Laws.BroadcastToContract<target, shape,
153 index => Replayed.value(shape, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, index))),
154 other => Replayed.value(shape, fill, ops, other),
155 Broadcast.broadcast_to(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, target)>:
156 +output = Shape.output_shape(plan)
157 +count = Shape.logical_numel(Shape.dimensions(output))
158 +total = Shape.logical_numel(Shape.dimensions(shape))
159 run_lift(shape, target, plan, planned, same, fill, ops,
160 result => Laws.BroadcastToContract<target, shape,
161 index => Replayed.value(shape, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, index))),
162 other => Replayed.value(shape, fill, ops, other), result>,
163 kept => kept_words => input_fits => output_ops => values => output_fits =>
164 Laws.BroadcastToContract{
165 {==},
166 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, dimensions => Some{dimensions}, Shape.dimensions(output), Shape.dimensions(target), same),
167 index => inside =>
168 +below = output_below(plan, target, index, same, inside)
169 Equal.trans(Maybe<&2, F32>,
170 Core.dynamic_read_value(Core.read_dynamic(Core.Packed{output, Core.TTensor{Replayed.storage(output, 0.0, output_ops), output_fits}}, index)),
171 Some{Replayed.value(output, 0.0, output_ops, index)},
172 Some{Replayed.value(shape, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, U32.to_nat(index))))},
173 PointwiseProof.replayed_point(output, 0.0, output_ops, output_fits, index, below),
174 Equal.trans(Maybe<&2, F32>, Some{Replayed.value(output, 0.0, output_ops, index)},
175 ReduceLaws.word_at(Laws.cells(plan, shape, fill, ops, count), U32.to_nat(index)),
176 Some{Replayed.value(shape, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, U32.to_nat(index))))},
177 listed_value(output, 0.0, output_ops, count, Laws.cells(plan, shape, fill, ops, count), index, values, below),
178 cells_at(plan, shape, fill, ops, count, U32.to_nat(index), below))),
179 other => inside =>
180 +within = {inside : {Nat.is_lt(U32.to_nat(other), total) == True{} : Bool}}
181 Equal.trans(Maybe<&2, F32>,
182 Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, kept), input_fits}}, other)),
183 Some{Replayed.value(shape, fill, kept, other)}, Some{Replayed.value(shape, fill, ops, other)},
184 PointwiseProof.replayed_point(shape, fill, kept, input_fits, other, within),
185 Equal.trans(Maybe<&2, F32>, Some{Replayed.value(shape, fill, kept, other)},
186 ReduceLaws.word_at(Contracts.words(shape, fill, ops, total), U32.to_nat(other)), Some{Replayed.value(shape, fill, ops, other)},
187 listed_value(shape, fill, kept, total, Contracts.words(shape, fill, ops, total), other, kept_words, within),
188 Equal.sym(Maybe<&2, F32>, Some{Replayed.value(shape, fill, ops, other)},
189 ReduceLaws.word_at(Contracts.words(shape, fill, ops, total), U32.to_nat(other)),
190 listed_value(shape, fill, ops, total, Contracts.words(shape, fill, ops, total), other, {==}, within))))})(fits)