def contribution_success

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:624

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwiseProof
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient

624def contribution_success(+shape: Shape.Shape, +index: U32, total: Core.Tensor<shape>,
625  pair: Core.Dynamic & Result<&2, &2, Core.Error, F32>,
626  -successful: {ElementwiseProof.dynamic_read_succeeded(pair) == True{} : Bool},
627  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
628  Holds<{step_continued(shape, Gradient.step_contribution(shape, index, total, pair)) == True{} : Bool}>:
629  (owner, result) = pair
630  match result:
631    case Fail{error}:
632      Holds{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
633    case Done{value}:
634      total_success(shape, index, owner, value, Core.read_flat(shape, total, index),
635        {\{TransformTotality.ReadSuccess: successful => successful} : TransformTotality.ReadSuccess<shape, total, index> ->
636          {TransformTotality.read_succeeded(shape, Core.read_flat(shape, total, index)) == True{} : Bool}}(
637          TransformProof.read_success_status(shape, total, index, TransformProof.read_success(shape, total, index, inside))),
638        inside)