GatherLAWS.gather_scatter_cells: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as GatherLAWS
Lines 305-339 of bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&start_line=305&end_line=339

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather

# For a balanced gradient array G, a balanced index array I and every split,
# the slot of the backward build that holds input cell (o, i, r), below the
# count, holds the gradient words of the cells (o, k, r) whose entry is i,
# added to +0.0 in increasing k, and +0.0 where no entry is i: PyTorch's
# one-thread index_add and scatter_add.
law gather_scatter_cells:
  for +depth: Nat
  for +splits: Nat
  for +kind: Gather.Lookup
  for +outer: Nat
  for +rows: Nat
  for +inner: Nat
  for +count: Nat
  for +cells: Nat
  for +base: Nat
  for +dg: Nat
  for -G: Array<F32>
  for g: Array<F32>
  for same: {g == G : Array<F32>}
  for valid: Model.Balanced(F32, dg, G)
  for +di: Nat
  for -I: Array<U32>
  for index: Array<U32>
  for same_index: {index == I : Array<U32>}
  for index_valid: Model.Balanced(U32, di, I)
  for +path: Model.Path(depth)
  for +o: Nat
  for +i: Nat
  for +r: Nat
  for i_below: {Nat.is_lt(i, rows) == True{} : Bool}
  for r_below: {Nat.is_lt(r, inner) == True{} : Bool}
  for at: {Nat.add(Model.offset(depth, path), base) == position(rows, inner, o, i, r) : Nat}
  for in_count: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), cells) == True{} : Bool}
  Summed<depth, Gather.scatter_build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, g, index), path,
    dg, G, di, I, kind, count, inner, o, i, r>

Uses (33):
  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=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  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.add
  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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  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=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Path
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Lookup
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=added
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=scatter_build
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=scatter_cell
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=scattered
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=Added
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=Summed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=position
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=AddedIs
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=added_is
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=scatter_cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=scattered_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact