def fiber_contract

bendtorch-core@0.1.0.0 · src/autograd/reduce_fold_PROOF.bend:216

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend as Fold
import bendtorch-core@0.1.0.0/src/tensor/contracts/fold_records.bend as Records
import bendtorch-core@0.1.0.0/src/tensor/contracts/sum.bend as Sum
import bendtorch-core@0.1.0.0/src/autograd/reduce_fold.bend as ReduceFold
import bendtorch-core@0.1.0.0/src/autograd/reduce_fold_LAWS.bend as Laws

216def fiber_contract(+plan: Shape.BroadcastPlan, +index: U32, +fill: F32, +ops: List<&2, StorageLaws.Op>,
217  -fits: {Lifecycle.logical_length(Replayed.storage(Shape.right_shape(plan), fill, ops)) ==
218    Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))) : Nat},
219  +expected: Maybe<&2, F32>, +total: F32, +count: Nat,
220  evidence: Records.FoldContract<Shape.right_shape(plan), total,
221    other => Replayed.value(Shape.right_shape(plan), fill, ops, other),
222    Fold.run(~Unit, ~Sum.add, ~ReduceFold.Cell, ~ReduceFold.source, ~ReduceFold.lands, Unit{}, ReduceFold.Cell{plan, index}, count,
223      Core.Packed{Shape.right_shape(plan), Core.TTensor{Replayed.storage(Shape.right_shape(plan), fill, ops), fits}})>,
224  equation: {expected == Some{total} : Maybe<&2, F32>}) ->
225  Laws.FiberContract<Shape.right_shape(plan), expected,
226    other => Replayed.value(Shape.right_shape(plan), fill, ops, other),
227    Fold.run(~Unit, ~Sum.add, ~ReduceFold.Cell, ~ReduceFold.source, ~ReduceFold.lands, Unit{}, ReduceFold.Cell{plan, index}, count,
228      Core.Packed{Shape.right_shape(plan), Core.TTensor{Replayed.storage(Shape.right_shape(plan), fill, ops), fits}})>:
229  Records.FoldContract{value, kept} = evidence
230  %Equal.sym(Maybe<&2, F32>, expected, Some{total}, equation) :
231    Laws.FiberContract<Shape.right_shape(plan), _,
232      other => Replayed.value(Shape.right_shape(plan), fill, ops, other),
233      Fold.run(~Unit, ~Sum.add, ~ReduceFold.Cell, ~ReduceFold.source, ~ReduceFold.lands, Unit{}, ReduceFold.Cell{plan, index}, count,
234        Core.Packed{Shape.right_shape(plan), Core.TTensor{Replayed.storage(Shape.right_shape(plan), fill, ops), fits}})>
235  Laws.FiberContract{value, kept}