PermuteBuildProof.owned_success: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteBuildProof
Lines 516-531 of bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&start_line=516&end_line=531

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/arith.bend as Arith
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/core.bend as Core
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

# An owned output has a cell, so a source of the same element count is owned.
def owned_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +d: Nat, +n: Nat,
  -valid: {Storage.bounds(d, n) == True{} : Bool}, -exact: {n == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}, source: Core.Tensor<input>) ->
  Fact<{Totality.copy_succeeded(input, axes, plan, Transforms.built_owned(input, axes, plan, d, n, valid, exact, source)) == True{} : Bool}>:
  Core.TTensor{storage, fits} = source
  match storage:
    case Storage.Empty{}:
      -positive = Arith.and_left(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d)),
        Arith.and_right(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d))), valid))
      Fact{Empty.absurd({False{} == True{} : Bool},
        Arith.lt_zero(0n,
          %Equal.sym(Nat, 0n, n, Equal.trans(Nat, 0n, Shape.logical_numel(Shape.dimensions(input)), n, fits,
            Equal.sym(Nat, n, Shape.logical_numel(Shape.dimensions(input)), Equal.trans(Nat, n, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Shape.logical_numel(Shape.dimensions(input)), exact, plan_numel(input, axes, plan))))) : {Nat.is_lt(0n, _) == True{} : Bool}
          positive))}
    case Storage.Owned{+ds, +ns, a, b, ok}:
      Fact{cloned_success(input, axes, plan, d, n, valid, exact, ds, ns, a, Array.clone(F32, a), {==}, b, ok, fits)}

Uses (29):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=lt_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=capacity
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=cloned_success
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=plan_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=copy_succeeded
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=built_owned