def scatter_slot

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:858

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel

858# The slot of input cell (o, i, r), below the count, holds what the gradient
859# target of the cell names.
860def scatter_slot(+depth: Nat, +splits: Nat, +plan: Slice.Plan, +count: Nat, +base: Nat, +dg: Nat, -G: Array<F32>, g: Array<F32>,
861  -same: {g == G : Array<F32>}, -valid: Model.Balanced(F32, dg, G), +path: Model.Path(depth),
862  -inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool}) ->
863  Parallel.Fact<{Model.observe(F32, depth, Slice.scatter_build(depth, splits, plan, count, base, g), path) ==
864    Some{Pair.fst(F32, Array<F32> & Array<F32>, Slice.scattered((G, empty()), Slice.target(plan, Nat.add(Model.offset(depth, path), base))))} :
865    Maybe<&2, F32>}>:
866  Parallel.Fact{
867    %inside :
868      {Model.observe(F32, depth, Slice.scatter_build(depth, splits, plan, count, base, g), path) ==
869        Some{Pair.fst(F32, Array<F32> & Array<F32>, Slice.scatter_cell(plan, Nat.add(Model.offset(depth, path), base), (G, empty()), _))} :
870        Maybe<&2, F32>}
871    {\{Parallel.Fact: q => q} : Parallel.Fact<ScatterCells(depth, splits, plan, count, base, G, g)> -> ScatterCells(depth, splits, plan, count, base, G, g)}(
872      scatter_cells(depth, splits, plan, count, base, dg, G, g, same, valid))(path)}