def owned_success

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

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

516# An owned output has a cell, so a source of the same element count is owned.
517def owned_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +d: Nat, +n: Nat,
518  -valid: {Storage.bounds(d, n) == True{} : Bool}, -exact: {n == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}, source: Core.Tensor<input>) ->
519  Fact<{Totality.copy_succeeded(input, axes, plan, Transforms.built_owned(input, axes, plan, d, n, valid, exact, source)) == True{} : Bool}>:
520  Core.TTensor{storage, fits} = source
521  match storage:
522    case Storage.Empty{}:
523      -positive = Arith.and_left(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d)),
524        Arith.and_right(Nat.is_le(d, 20n), Bool.and(Nat.is_lt(0n, n), Nat.is_le(n, Model.capacity(d))), valid))
525      Fact{Empty.absurd({False{} == True{} : Bool},
526        Arith.lt_zero(0n,
527          %Equal.sym(Nat, 0n, n, Equal.trans(Nat, 0n, Shape.logical_numel(Shape.dimensions(input)), n, fits,
528            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}
529          positive))}
530    case Storage.Owned{+ds, +ns, a, b, ok}:
531      Fact{cloned_success(input, axes, plan, d, n, valid, exact, ds, ns, a, Array.clone(F32, a), {==}, b, ok, fits)}