law slice_build_cells

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

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

330# For a balanced input array A and every split, the slot of the forward
331# build that holds output cell (o, k, r), below the count, holds input cell
332# (o, start + k * step, r): the word PyTorch's slice puts there.
333law slice_build_cells:
334  for +depth: Nat
335  for +splits: Nat
336  for +outer: Nat
337  for +extent: Nat
338  for +inner: Nat
339  for +start: Nat
340  for +step: Nat
341  for +length: Nat
342  for +count: Nat
343  for +base: Nat
344  for +da: Nat
345  for -A: Array<F32>
346  for a: Array<F32>
347  for same: {a == A : Array<F32>}
348  for valid: Model.Balanced(F32, da, A)
349  for +path: Model.Path(depth)
350  for +o: Nat
351  for +k: Nat
352  for +r: Nat
353  for k_below: {Nat.is_lt(k, length) == True{} : Bool}
354  for r_below: {Nat.is_lt(r, inner) == True{} : Bool}
355  for at: {Nat.add(Model.offset(depth, path), base) == position(length, inner, o, k, r) : Nat}
356  for inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool}
357  Holds<{Model.observe(F32, depth, Slice.build(depth, splits, Slice.Plan{outer, extent, inner, start, step, length}, count, base, a), path) ==
358    Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(position(extent, inner, o, Nat.add(start, Nat.mul(k, step)), r)))) :
359    Maybe<&2, F32>}>