def rows_mapping

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:291

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/tensor/elementwise_parallel_proof.bend as Parallel

291def rows_mapping(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
292  -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
293  -kept: Core.Tensor<shape>, -array: Array<F32>, -taken: Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, array)>,
294  +rows: List<&2, Shape.Row>,
295  +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>},
296  +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
297  +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
298  +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
299  Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan},
300    Reduce.parallel_rows(plan, target, depth, length, valid, exact, (Core.Packed{shape, kept}, array), rows))>:
301  Holds{({==}, values => listed => index => inside =>
302    {\{Parallel.Taken: d => balanced => reads => retained =>
303      {\{Holds: proof => proof} :
304        Holds<{Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
305          Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}> ->
306        {Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
307          Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(
308        rows_cell(shape, tensor, target, plan, depth, length, valid, exact, rows, rows_exact, array, d, balanced, reads, left, right, count,
309          values, listed, index, inside))} :
310      Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, array)> ->
311      {Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
312        Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(taken))}