law permute_contract

bendtorch-core@0.1.0.0 · src/tensor/permute_values_contract_LAWS.bend:12

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/permute_values_records.bend as Records
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core

12# `permute_copy` of a `Core.from_values(input, values)` tensor by a valid
13# permutation succeeds with dimensions `Axis.order(dims, axes)`; output index i
14# holds `values[permute_source(input, axes, i)]`, and the returned source
15# still holds `values[j]` at every j.
16law permute_contract:
17  for +input: Shape.Shape
18  for +values: List<&2, F32>
19  for counted: {List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(input)) : Nat}
20  for +axes: List<&2, U32>
21  for valid: {True{} == Layout.bijective(input, axes) : Bool}
22  Records.PermuteContract<input, values, axes>