def one_contract

bendtorch-core@0.1.0.0 · src/autograd/tensor_vjp_PROOF.bend:1059

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/pointwise_proof.bend as PointwiseProof
import bendtorch-core@0.1.0.0/src/autograd/sum_to_size_fold_PROOF.bend as SumToSizeFoldProof
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_LAWS.bend as Laws

1059# A delivered contribution, a replayed tensor with its target's dimensions
1060# whose cells hold the stated words, meets the one-contribution contract.
1061def one_contract(+a: Nat, +target: Shape.Shape, -target_cell: U32 -> Maybe<&2, F32>, -saved: Backward.Saved, -g: Core.Dynamic,
1062  +first: Shape.Shape, +first_dimensions: {Shape.dimensions(first) == Shape.dimensions(target) : List<&2, U32>},
1063  +first_fill: F32, +first_ops: List<&2, StorageLaws.Op>,
1064  first_values: @+index: U32 -> @inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool} ->
1065    {Some{Replayed.value(first, first_fill, first_ops, index)} == target_cell(index) : Maybe<&2, F32>},
1066  -first_fits: {Lifecycle.logical_length(Replayed.storage(first, first_fill, first_ops)) == Shape.logical_numel(Shape.dimensions(first)) : Nat}) ->
1067  Laws.OneContract<a, target, target_cell,
1068    Backward.Pass{saved, g, Done{[Backward.Contribution{a, target, Core.Packed{first, Core.TTensor{Replayed.storage(first, first_fill, first_ops), first_fits}}}]}}>:
1069  Laws.OneContract{
1070    {==},
1071    Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, dimensions => Some{dimensions}, Shape.dimensions(first), Shape.dimensions(target),
1072      first_dimensions),
1073    index => inside =>
1074      +inside = inside
1075      Equal.trans(Maybe<&2, F32>,
1076        Core.dynamic_read_value(Core.read_dynamic(Core.Packed{first, Core.TTensor{Replayed.storage(first, first_fill, first_ops), first_fits}}, index)),
1077        Some{Replayed.value(first, first_fill, first_ops, index)}, target_cell(index),
1078        PointwiseProof.replayed_point(first, first_fill, first_ops, first_fits, index,
1079          SumToSizeFoldProof.shape_below(first, target, index, first_dimensions, inside)),
1080        first_values(index, inside))}