def rows_cell
bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:230
import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
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/autograd/reduce.bend as Reduce
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallel
230def rows_cell(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
231 -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
232 +rows: List<&2, Shape.Row>,
233 +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>},
234 -array: Array<F32>, +d: Nat, -balanced: Model.Balanced(F32, d, array), -reads: Parallel.SourceReads(Core.Packed{shape, tensor}, d, array),
235 +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
236 +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
237 +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
238 +values: List<&2, F32>, -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +index: U32,
239 +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}) ->
240 Holds<{Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
241 Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}>:
242 +t = U32.to_nat(index)
243 +extents = Shape.extents(Shape.output_shape(plan))
244 +splits = Reduce.splits(plan, depth, length)
245 -built = parallel_build(plan, depth, length, rows, array)
246 -inside_length : {Nat.is_lt(t, length) == True{} : Bool} =
247 %Equal.sym(Nat, length, Shape.logical_numel(Shape.dimensions(target)), exact) : {Nat.is_lt(t, _) == True{} : Bool}
248 inside
249 +path = Refinement.route(depth, index)
250 Holds{{\{ReduceParallel.CellAt: word => observed => words => seen => total =>
251 Equal.trans(Maybe<&2, F32>, Lifecycle.observe_allowed(depth, length, built, index, Nat.is_lt(t, length)),
252 Model.observe(F32, depth, built, path), Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))),
253 Parallel.observe_allowed_equal(depth, length, built, index, Nat.is_lt(t, length), inside_length,
254 Equal.sym(Bool, True{}, Storage.index_matches(depth, length, index), Route.index_complete(depth, length, index, valid, inside_length))),
255 %Equal.sym(Maybe<&2, F32>, Model.observe(F32, depth, built, path), Some{word}, observed) :
256 {_ == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}
257 %Equal.sym(F32, word, ReduceParallel.fsum(words, 0.0), total) :
258 {Some{_} == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}
259 %count : {Some{ReduceParallel.fsum(words, 0.0)} == Laws.fiber(plan, values, index, _) : Maybe<&2, F32>}
260 {\{Parallel.Fact: p => p} :
261 Parallel.Fact<{Some{ReduceParallel.fsum(words, 0.0)} == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : Maybe<&2, F32>}> ->
262 {Some{ReduceParallel.fsum(words, 0.0)} == Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : Maybe<&2, F32>}}(
263 ReduceParallel.cell_value(plan, rows, rows_exact, values, index, d, array, words, seen,
264 %Equal.sym(List<&2, U32>, Shape.dimensions(Shape.left_shape(plan)), Shape.dimensions(target), left) :
265 {Nat.is_lt(t, Shape.logical_numel(_)) == True{} : Bool}
266 inside,
267 position => below =>
268 +shaped : {Nat.is_lt(position, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool} =
269 %right : {Nat.is_lt(position, Shape.logical_numel(_)) == True{} : Bool}
270 below
271 +exact_word = MatrixIndex.word_exact(position, shape, shaped)
272 Equal.trans(Maybe<&2, F32>, Model.observe(F32, d, array, Refinement.route(d, U32.from_nat(position))),
273 Core.checked_observe_dynamic(Core.Packed{shape, tensor}, U32.from_nat(position)), Laws.word_at(values, position),
274 reads(U32.from_nat(position))(
275 %Equal.sym(Nat, U32.to_nat(U32.from_nat(position)), position, exact_word) :
276 {Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
277 shaped),
278 %exact_word :
279 {Core.checked_observe_dynamic(Core.Packed{shape, tensor}, U32.from_nat(position)) == Laws.word_at(values, _) : Maybe<&2, F32>}
280 listed(U32.from_nat(position))))))} :
281 ReduceParallel.CellAt<d, array, rows, extents, t, Model.observe(F32, depth, built, path)> ->
282 {Lifecycle.observe_allowed(depth, length, built, index, Nat.is_lt(t, length)) ==
283 Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(
284 %inside_length : ReduceParallel.CellSpec(d, array, rows, extents, t, _, Model.observe(F32, depth, built, path))
285 %Parallel.output_position(depth, length, index, valid, inside_length) :
286 ReduceParallel.CellIs(d, array, rows, extents, length, _, Model.observe(F32, depth, built, path))
287 {\{Parallel.Fact: p => p} :
288 Parallel.Fact<ReduceParallel.Cells(depth, d, array, rows, extents, length, 0n, built)> -> ReduceParallel.Cells(depth, d, array, rows, extents, length, 0n, built)}(
289 ReduceParallel.build_cells(depth, splits, d, array, rows, extents, length, 0n, array, {==}, balanced))(path))}