ReduceReplayedProof.word_fiber: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend as ReduceReplayedProof
Lines 1094-1116 of bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&start_line=1094&end_line=1116

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/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws
import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as Fiber
import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallel

def word_fiber(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +index: U32,
  +inside: {Nat.is_lt(U32.to_nat(index), Shape.numel(Shape.extents(Shape.left_shape(plan)))) == True{} : Bool},
  +right: {Shape.dimensions(Shape.right_shape(plan)) == Shape.dimensions(shape) : List<&2, U32>}) ->
  {Some{cell_word(plan, map, shape, fill, ops, U32.to_nat(index))} ==
    ReduceLaws.fiber(plan, Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))), index,
      Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) : Maybe<&2, F32>}:
  match map:
    case Shape.Unindexed{zero}:
      %zero : {Some{0.0} == ReduceLaws.fiber(plan, Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))), index, _) : Maybe<&2, F32>}
      {==}
    case Shape.Indexed{+rows, +rows_exact}:
      +t = U32.to_nat(index)
      +output = Shape.extents(Shape.output_shape(plan))
      +count = Shape.numel(output)
      +values = Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape)))
      +walk = ReduceParallel.plan_walk(plan, rows, rows_exact, t, inside)
      %Equal.sym(Maybe<&2, F32>, ReduceLaws.fiber(plan, values, index, count), ReduceParallel.gather(values, Fiber.masked(count, rows, t, 0n, 0n), Some{0.0}),
        ReduceParallel.fiber_masked(plan, rows, rows_exact, values, index, count, Conversion.le_reflexive(count))) :
        {Some{rfold(shape, fill, ops, ReduceParallel.visited_of(rows, output, t), 0.0)} == _ : Maybe<&2, F32>}
      %Equal.sym(List<&2, Nat>, Fiber.masked(count, rows, t, 0n, 0n), ReduceParallel.visited_of(rows, output, t), walk) :
        {Some{rfold(shape, fill, ops, ReduceParallel.visited_of(rows, output, t), 0.0)} == ReduceParallel.gather(values, _, Some{0.0}) : Maybe<&2, F32>}
      rfold_gather(shape, fill, ops, ReduceParallel.visited_of(rows, output, t), 0.0,
        walk_below(plan, rows, rows_exact, shape, Shape.numel(Shape.extents(Shape.left_shape(plan))), Facts{{==}, right}, t, inside))

Uses (34):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=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_LAWS.bend&name=fiber
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=fiber_masked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=gather
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=plan_walk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=visited_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=Facts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=PlanMap
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=cell_word
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=rfold
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=rfold_gather
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=walk_below
  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=Index
  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=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=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/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/word_conversion.bend&name=le_reflexive