ReduceFoldPROOF.fiber_total: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend as ReduceFoldPROOF Lines 145-184 of bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend&start_line=145&end_line=184 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 def fiber_total(+plan: Shape.BroadcastPlan, +index: U32, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat, +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}) -> {ReduceLaws.fiber(plan, Contracts.words(Shape.right_shape(plan), fill, ops, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))), index, count) == Some{Fold.total(~Unit, ~Sum.add, ~ReduceFold.Cell, ~ReduceFold.source, ~ReduceFold.lands, Unit{}, ReduceFold.Cell{plan, index}, Shape.right_shape(plan), fill, ops, count)} : Maybe<&2, F32>}: match count: case 0n: {==} case 1n+k: +right = Shape.right_shape(plan) +output = Shape.output_shape(plan) +limit = Shape.logical_numel(Shape.dimensions(output)) +values = Contracts.words(right, fill, ops, Shape.logical_numel(Shape.dimensions(right))) +cell : ReduceFold.Cell = ReduceFold.Cell{plan, index} +lm = ReduceFold.target_offset(plan, k) +rm = ReduceFold.contribution_offset(plan, k) +before = Fold.total(~Unit, ~Sum.add, ~ReduceFold.Cell, ~ReduceFold.source, ~ReduceFold.lands, Unit{}, cell, right, fill, ops, k) +word = Replayed.value(right, fill, ops, U32.from_nat(rm)) +lands = Nat.is_eq(lm, U32.to_nat(index)) +after : Maybe<&2, F32> = Some{Fold.chosen(~Unit, ~Sum.add, Unit{}, lands, before, word)} +below = Conversion.le_successor_lt(k, limit, room) +rm_below = BroadcastProof.right_walk_bound(plan, Shape.index_map(plan), k, below) +lm_below = BroadcastProof.left_walk_bound(plan, Shape.index_map(plan), k, below) %Equal.sym(Maybe<&1, U32 & U32>, Projection.offset_spec(plan, k), Some{(U32.from_nat(lm), U32.from_nat(rm))}, offsets_walk(plan, Shape.index_map(plan), k, BroadcastProof.output_inside(plan, k, below))) : {ReduceLaws.contribute(values, index, ReduceLaws.fiber(plan, values, index, k), _) == after : Maybe<&2, F32>} %Equal.sym(Maybe<&2, F32>, ReduceLaws.fiber(plan, values, index, k), Some{before}, fiber_total(plan, index, fill, ops, k, Conversion.le_predecessor(k, limit, room))) : {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))) == after : Maybe<&2, F32>} %Equal.sym(Nat, U32.to_nat(U32.from_nat(rm)), rm, PointwiseProof.word_exact(rm, right, rm_below)) : {ReduceLaws.matched(Some{before}, ReduceLaws.word_at(values, _), Nat.is_eq(U32.to_nat(U32.from_nat(lm)), U32.to_nat(index))) == after : Maybe<&2, F32>} %Equal.sym(Maybe<&2, F32>, ReduceLaws.word_at(values, rm), Some{word}, words_at(right, fill, ops, Shape.logical_numel(Shape.dimensions(right)), rm, rm_below)) : {ReduceLaws.matched(Some{before}, _, Nat.is_eq(U32.to_nat(U32.from_nat(lm)), U32.to_nat(index))) == after : Maybe<&2, F32>} %Equal.sym(Nat, U32.to_nat(U32.from_nat(lm)), lm, PointwiseProof.word_exact(lm, Shape.left_shape(plan), lm_below)) : {ReduceLaws.matched(Some{before}, Some{word}, Nat.is_eq(_, U32.to_nat(index))) == after : Maybe<&2, F32>} matched_chosen(lands, before, word) Uses (46): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym 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=Maybe 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=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma 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=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=contribute https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=fiber https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=matched https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=word_at https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold.bend&name=Cell https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold.bend&name=contribution_offset https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold.bend&name=lands https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold.bend&name=source https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold.bend&name=target_offset https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend&name=matched_chosen https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend&name=offsets_walk https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend&name=words_at 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=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_map https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=left_shape 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/shape/core.bend&name=right_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/tensor/contracts/LAWS.bend&name=words https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast_proof.bend&name=left_walk_bound https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast_proof.bend&name=output_inside https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast_proof.bend&name=right_walk_bound https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend&name=chosen https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend&name=total https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend&name=word_exact 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/contracts/sum.bend&name=add https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend&name=offset_spec https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_predecessor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_successor_lt