law slice_scatter_miss

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

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

393# ... and the slot of input cell (o, i, r) where no k below the length has
394# i = start + k * step holds +0.0, as PyTorch's slice_backward leaves it.
395law slice_scatter_miss:
396  for +depth: Nat
397  for +splits: Nat
398  for +outer: Nat
399  for +extent: Nat
400  for +inner: Nat
401  for +start: Nat
402  for +step: Nat
403  for +length: Nat
404  for +count: Nat
405  for +base: Nat
406  for +dg: Nat
407  for -G: Array<F32>
408  for g: Array<F32>
409  for same: {g == G : Array<F32>}
410  for valid: Model.Balanced(F32, dg, G)
411  for +path: Model.Path(depth)
412  for +o: Nat
413  for +i: Nat
414  for +r: Nat
415  for i_below: {Nat.is_lt(i, extent) == True{} : Bool}
416  for r_below: {Nat.is_lt(r, inner) == True{} : Bool}
417  for missed: @+k: Nat -> @below: {Nat.is_lt(k, length) == True{} : Bool} ->
418    {Nat.is_eq(Nat.add(start, Nat.mul(k, step)), i) == False{} : Bool}
419  for at: {Nat.add(Model.offset(depth, path), base) == position(extent, inner, o, i, r) : Nat}
420  for inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool}
421  Holds<{Model.observe(F32, depth, Slice.scatter_build(depth, splits, Slice.Plan{outer, extent, inner, start, step, length}, count, base, g), path) ==
422    Some{0.0} : Maybe<&2, F32>}>