def cloned_success

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:507

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/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality

507def cloned_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +d: Nat, +n: Nat,
508  -valid: {Storage.bounds(d, n) == True{} : Bool}, -exact: {n == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat},
509  +ds: Nat, +ns: Nat, -a: Array<F32>, pair: Array<F32> & Array<F32>, -same: {pair == Array.clone(F32, a) : Array<F32> & Array<F32>},
510  -b: Model.Balanced(F32, ds, a), -ok: {Storage.bounds(ds, ns) == True{} : Bool},
511  -fits: {Lifecycle.logical_length(Storage.Owned{ds, ns, a, b, ok}) == Shape.logical_numel(Shape.dimensions(input)) : Nat}) ->
512  {Totality.copy_succeeded(input, axes, plan, Transforms.built_cloned(input, axes, plan, d, n, valid, exact, ds, ns, a, pair, same, b, ok, fits)) == True{} : Bool}:
513  (kept, copy) = pair
514  {==}