law slice_scatter_hit

bendtorch-core@0.1.0.0 · src/tensor/slice_LAWS.bend:361

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

361# For a balanced gradient array G and every split, the slot of the backward
362# build that holds input cell (o, start + k * step, r), with k below the
363# length and a positive step, holds gradient cell (o, k, r) ...
364law slice_scatter_hit:
365  for +depth: Nat
366  for +splits: Nat
367  for +outer: Nat
368  for +extent: Nat
369  for +inner: Nat
370  for +start: Nat
371  for +step: Nat
372  for +length: Nat
373  for +count: Nat
374  for +base: Nat
375  for +dg: Nat
376  for -G: Array<F32>
377  for g: Array<F32>
378  for same: {g == G : Array<F32>}
379  for valid: Model.Balanced(F32, dg, G)
380  for +path: Model.Path(depth)
381  for +o: Nat
382  for +k: Nat
383  for +r: Nat
384  for positive: {Nat.is_lt(0n, step) == True{} : Bool}
385  for k_below: {Nat.is_lt(k, length) == True{} : Bool}
386  for i_below: {Nat.is_lt(Nat.add(start, Nat.mul(k, step)), extent) == True{} : Bool}
387  for r_below: {Nat.is_lt(r, inner) == True{} : Bool}
388  for at: {Nat.add(Model.offset(depth, path), base) == position(extent, inner, o, Nat.add(start, Nat.mul(k, step)), r) : Nat}
389  for inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool}
390  Holds<{Model.observe(F32, depth, Slice.scatter_build(depth, splits, Slice.Plan{outer, extent, inner, start, step, length}, count, base, g), path) ==
391    Model.observe(F32, dg, G, Refinement.route(dg, U32.from_nat(position(length, inner, o, k, r)))) : Maybe<&2, F32>}>