ReducePROOF.rows_mapping: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
Lines 291-312 of bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&start_line=291&end_line=312

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

def rows_mapping(+shape: Shape.Shape, -tensor: Core.Tensor<shape>, +target: Shape.Shape, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat,
  -valid: {Storage.bounds(depth, length) == True{} : Bool}, -exact: {length == Shape.logical_numel(Shape.dimensions(target)) : Nat},
  -kept: Core.Tensor<shape>, -array: Array<F32>, -taken: Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, array)>,
  +rows: List<&2, Shape.Row>,
  +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>},
  +left: {Shape.dimensions(Shape.left_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
  +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>},
  +count: {Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
  Holds<Laws.MappingWith(Core.Packed{shape, tensor}, target, Done{plan},
    Reduce.parallel_rows(plan, target, depth, length, valid, exact, (Core.Packed{shape, kept}, array), rows))>:
  Holds{({==}, values => listed => index => inside =>
    {\{Parallel.Taken: d => balanced => reads => retained =>
      {\{Holds: proof => proof} :
        Holds<{Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
          Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}> ->
        {Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
          Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(
        rows_cell(shape, tensor, target, plan, depth, length, valid, exact, rows, rows_exact, array, d, balanced, reads, left, right, count,
          values, listed, index, inside))} :
      Parallel.Taken<Core.Packed{shape, tensor}, (Core.Packed{shape, kept}, array)> ->
      {Lifecycle.observe_allowed(depth, length, parallel_build(plan, depth, length, rows, array), index, Nat.is_lt(U32.to_nat(index), length)) ==
        Laws.fiber(plan, values, index, Shape.logical_numel(Shape.dimensions(shape))) : Maybe<&2, F32>}}(taken))}

Uses (32):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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/reduce.bend&name=parallel_rows
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=MappingWith
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=fiber
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=parallel_build
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend&name=rows_cell
  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=Row
  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=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_table
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=left_shape
  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/shape/core.bend&name=right_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds
  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_parallel_proof.bend&name=Taken
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=observe_allowed