def tensor_preserved

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:469

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
import bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage

469# The tensor the fold hands back holds every word it held.
470def tensor_preserved(-shape: Shape.Shape, +fuel: Nat, tensor: Core.Tensor<shape>) ->
471  Fact<Laws.Preserved<shape, tensor, Reduction.tensor_sum(shape, fuel, tensor)>>:
472  Core.TTensor{storage, exact} = tensor
473  match storage:
474    case Storage.Empty{}:
475      Fact{Laws.Preserved{other => {==}}}
476    case Storage.Owned{+depth, +length, array, balanced, valid}:
477      owned_preserved(shape, depth, length, array, balanced, valid, exact, Reduction.array_sum(fuel, 0n, 0.0, array),
478        Reduction.array_sum_keeps(depth, array, balanced, fuel, 0n, 0.0, array, {==}))