GatherPROOF.scatter_keeps: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
Lines 579-591 of bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&start_line=579&end_line=591

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
import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

# A backward cell runs the sum from +0.0 over every k and hands both arrays
# back.
def scatter_keeps(+kind: Gather.Lookup, +outer: Nat, +rows: Nat, +inner: Nat, +count: Nat, +at: Nat, +dg: Nat, -G: Array<F32>, +di: Nat,
  -I: Array<U32>, inside: Bool, -valid: Model.Balanced(F32, dg, G), -index_valid: Model.Balanced(U32, di, I)) ->
  Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.scatter_cell(Gather.Plan{kind, outer, rows, inner, count}, at, (G, I), inside)) == (G, I) : Array<F32> & Array<U32>}>:
  match inside:
    case False{}:
      Generic.Fact{{==}}
    case True{}:
      Generic.Fact{Pair.fst({Pair.snd(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, (0.0, (G, I)))) == (G, I) : Array<F32> & Array<U32>},
        Laws.Added(dg, G, di, I, kind, count, inner, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, 0.0, Pair.fst(F32, Array<F32> & Array<U32>, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, (0.0, (G, I))))),
        {\{Generic.Fact: q => q} : Generic.Fact<AddedIs(dg, G, di, I, kind, outer, rows, inner, count, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, 0.0, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, (0.0, (G, I))))> -> AddedIs(dg, G, di, I, kind, outer, rows, inner, count, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, 0.0, Gather.added(Gather.Plan{kind, outer, rows, inner, count}, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, (0.0, (G, I))))}(
          added_is(dg, G, di, I, kind, outer, rows, inner, count, Nat.div(Nat.div(at, inner), rows), Nat.mod(Nat.div(at, inner), rows), Nat.mod(at, inner), count, 0n, 0.0, valid, index_valid)))}

Uses (20):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  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/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_cell
  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_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/parallel_proofs.bend&name=Fact