def fiber_total
bendtorch-core@0.1.0.0 · src/autograd/reduce_fold_PROOF.bend:145
import bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend as ReduceFoldPROOF
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/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Projection
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/tensor/contracts/broadcast_proof.bend as BroadcastProof
import bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend as Fold
import bendtorch-core@0.1.0.0/src/tensor/contracts/sum.bend as Sum
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws
import bendtorch-core@0.1.0.0/src/autograd/reduce_fold.bend as ReduceFold
145def fiber_total(+plan: Shape.BroadcastPlan, +index: U32, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat,
146 +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}) ->
147 {ReduceLaws.fiber(plan,
148 Contracts.words(Shape.right_shape(plan), fill, ops, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))), index, count) ==
149 Some{Fold.total(~Unit, ~Sum.add, ~ReduceFold.Cell, ~ReduceFold.source, ~ReduceFold.lands, Unit{}, ReduceFold.Cell{plan, index},
150 Shape.right_shape(plan), fill, ops, count)} : Maybe<&2, F32>}:
151 match count:
152 case 0n:
153 {==}
154 case 1n+k:
155 +right = Shape.right_shape(plan)
156 +output = Shape.output_shape(plan)
157 +limit = Shape.logical_numel(Shape.dimensions(output))
158 +values = Contracts.words(right, fill, ops, Shape.logical_numel(Shape.dimensions(right)))
159 +cell : ReduceFold.Cell = ReduceFold.Cell{plan, index}
160 +lm = ReduceFold.target_offset(plan, k)
161 +rm = ReduceFold.contribution_offset(plan, k)
162 +before = Fold.total(~Unit, ~Sum.add, ~ReduceFold.Cell, ~ReduceFold.source, ~ReduceFold.lands, Unit{}, cell, right, fill, ops, k)
163 +word = Replayed.value(right, fill, ops, U32.from_nat(rm))
164 +lands = Nat.is_eq(lm, U32.to_nat(index))
165 +after : Maybe<&2, F32> = Some{Fold.chosen(~Unit, ~Sum.add, Unit{}, lands, before, word)}
166 +below = Conversion.le_successor_lt(k, limit, room)
167 +rm_below = BroadcastProof.right_walk_bound(plan, Shape.index_map(plan), k, below)
168 +lm_below = BroadcastProof.left_walk_bound(plan, Shape.index_map(plan), k, below)
169 %Equal.sym(Maybe<&1, U32 & U32>, Projection.offset_spec(plan, k), Some{(U32.from_nat(lm), U32.from_nat(rm))},
170 offsets_walk(plan, Shape.index_map(plan), k, BroadcastProof.output_inside(plan, k, below))) :
171 {ReduceLaws.contribute(values, index, ReduceLaws.fiber(plan, values, index, k), _) == after : Maybe<&2, F32>}
172 %Equal.sym(Maybe<&2, F32>, ReduceLaws.fiber(plan, values, index, k), Some{before},
173 fiber_total(plan, index, fill, ops, k, Conversion.le_predecessor(k, limit, room))) :
174 {ReduceLaws.matched(_, ReduceLaws.word_at(values, U32.to_nat(U32.from_nat(rm))), Nat.is_eq(U32.to_nat(U32.from_nat(lm)), U32.to_nat(index))) ==
175 after : Maybe<&2, F32>}
176 %Equal.sym(Nat, U32.to_nat(U32.from_nat(rm)), rm, PointwiseProof.word_exact(rm, right, rm_below)) :
177 {ReduceLaws.matched(Some{before}, ReduceLaws.word_at(values, _), Nat.is_eq(U32.to_nat(U32.from_nat(lm)), U32.to_nat(index))) ==
178 after : Maybe<&2, F32>}
179 %Equal.sym(Maybe<&2, F32>, ReduceLaws.word_at(values, rm), Some{word},
180 words_at(right, fill, ops, Shape.logical_numel(Shape.dimensions(right)), rm, rm_below)) :
181 {ReduceLaws.matched(Some{before}, _, Nat.is_eq(U32.to_nat(U32.from_nat(lm)), U32.to_nat(index))) == after : Maybe<&2, F32>}
182 %Equal.sym(Nat, U32.to_nat(U32.from_nat(lm)), lm, PointwiseProof.word_exact(lm, Shape.left_shape(plan), lm_below)) :
183 {ReduceLaws.matched(Some{before}, Some{word}, Nat.is_eq(_, U32.to_nat(index))) == after : Maybe<&2, F32>}
184 matched_chosen(lands, before, word)