TensorBackwardPROOF.sum_dims_decided: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend as TensorBackwardPROOF Lines 490-510 of bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&start_line=490&end_line=510 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/storage/arith.bend as Arith import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend as Laws import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend as PointwiseBroadcast import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws def sum_dims_decided(+a: Nat, +shape: Shape.Shape, +input: Shape.Shape, +kept: Shape.Shape, +plan: Shape.BroadcastPlan, planned: {Shape.broadcast_checked(kept, input) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, same: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(input) : List<&2, U32>}, counted: {Nat.is_eq(Shape.elements(shape), Shape.elements(kept)) == True{} : Bool}, saved: Backward.Saved, +fill: F32, +ops: List<&2, StorageLaws.Op>, -fits: {Lifecycle.logical_length(Replayed.storage(kept, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, decision: Shape.BoolCase) -> Laws.SoleContract Replayed.value(kept, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, index))), Backward.unsqueezed(a, input, kept, shape, Core.TTensor{Replayed.storage(kept, fill, ops), fits}, decision)>: match decision: case Shape.BFalse{equal}: Empty.absurd(Laws.SoleContract Replayed.value(kept, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, index))), Backward.unsqueezed(a, input, kept, shape, Core.TTensor{Replayed.storage(kept, fill, ops), fits}, Shape.BFalse{equal})>, Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.elements(shape), Shape.elements(kept)), True{}, equal, counted))) case Shape.BTrue{equal}: restored_contract(a, input, index => Replayed.value(kept, fill, ops, U32.from_nat(PointwiseBroadcast.left_map(plan, index))), shape, Backward.vjp_sum(a, input, Transforms.reshape_equal(shape, kept, Core.TTensor{Replayed.storage(kept, fill, ops), fits}, Transforms.elements_equal(shape, kept, equal))), Laws.tensor_sum_vjp_pointwise(a, kept, input, plan, planned, same, saved, fill, ops, Equal.trans(Nat, Lifecycle.logical_length(Replayed.storage(kept, fill, ops)), Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(kept)), fits, Transforms.elements_equal(shape, kept, equal)))) Uses (34): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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.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_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Saved https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=unsqueezed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=vjp_sum https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend&name=SoleContract https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend&name=tensor_sum_vjp_pointwise https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&name=restored_contract https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Error 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=broadcast_checked 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=elements 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/shape/core.bend&name=output_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend&name=left_map https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=storage https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=value 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/lifecycle.bend&name=logical_length https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=elements_equal https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=reshape_equal