ReduceParallelProof.fiber_masked: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof Lines 140-188 of bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&start_line=140&end_line=188 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape 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/broadcast_proof.bend as BroadcastProof import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as Fiber # The masked fold of `ReduceLaws.fiber` adds, in order, the words at the # masked positions. def fiber_masked(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>, +exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>}, +values: List<&2, F32>, +index: U32, +count: Nat, +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}) -> {ReduceLaws.fiber(plan, values, index, count) == gather(values, Fiber.masked(count, rows, U32.to_nat(index), 0n, 0n), Some{0.0}) : Maybe<&2, F32>}: match count: case 0n: {==} case 1n+k: +t = U32.to_nat(index) +map : Shape.Index = Shape.Indexed{rows, exact} +limit = Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) +below = Conversion.le_successor_lt(k, limit, room) +lm = Shape.walk_left(rows, k) +rm = Shape.walk_right(rows, k) +before = Fiber.masked(k, rows, t, 0n, 0n) +last = Fiber.kept(Nat.is_eq(lm, t), rm, Nil{}) +lm_below = BroadcastProof.left_walk_bound(plan, map, k, below) +rm_below = BroadcastProof.right_walk_bound(plan, map, 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, map, k, BroadcastProof.output_inside(plan, k, below))) : {ReduceLaws.contribute(values, index, ReduceLaws.fiber(plan, values, index, k), _) == gather(values, Fiber.masked(1n+k, rows, t, 0n, 0n), Some{0.0}) : Maybe<&2, F32>} %Equal.sym(Nat, U32.to_nat(U32.from_nat(rm)), rm, PointwiseProof.word_exact(rm, Shape.right_shape(plan), rm_below)) : {ReduceLaws.matched(ReduceLaws.fiber(plan, values, index, k), ReduceLaws.word_at(values, _), Nat.is_eq(U32.to_nat(U32.from_nat(lm)), t)) == gather(values, Fiber.masked(1n+k, rows, t, 0n, 0n), Some{0.0}) : 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(ReduceLaws.fiber(plan, values, index, k), ReduceLaws.word_at(values, rm), Nat.is_eq(_, t)) == gather(values, Fiber.masked(1n+k, rows, t, 0n, 0n), Some{0.0}) : Maybe<&2, F32>} %Equal.sym(Maybe<&2, F32>, ReduceLaws.fiber(plan, values, index, k), gather(values, before, Some{0.0}), fiber_masked(plan, rows, exact, values, index, k, Conversion.le_predecessor(k, limit, room))) : {ReduceLaws.matched(_, ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)) == gather(values, Fiber.masked(1n+k, rows, t, 0n, 0n), Some{0.0}) : Maybe<&2, F32>} %succ_add(k) : {ReduceLaws.matched(gather(values, before, Some{0.0}), ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)) == gather(values, Fiber.masked(_, rows, t, 0n, 0n), Some{0.0}) : Maybe<&2, F32>} %Equal.sym(List<&2, Nat>, Fiber.masked(Nat.add(k, 1n), rows, t, 0n, 0n), List.append(&2, Nat, before, Fiber.masked(1n, rows, t, 0n, Nat.add(0n, k))), Fiber.masked_split(k, 1n, rows, t, 0n, 0n)) : {ReduceLaws.matched(gather(values, before, Some{0.0}), ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)) == gather(values, _, Some{0.0}) : Maybe<&2, F32>} %Equal.sym(Maybe<&2, F32>, gather(values, List.append(&2, Nat, before, last), Some{0.0}), gather(values, last, gather(values, before, Some{0.0})), gather_append(values, before, last, Some{0.0})) : {ReduceLaws.matched(gather(values, before, Some{0.0}), ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)) == _ : Maybe<&2, F32>} Equal.sym(Maybe<&2, F32>, gather(values, last, gather(values, before, Some{0.0})), ReduceLaws.matched(gather(values, before, Some{0.0}), ReduceLaws.word_at(values, rm), Nat.is_eq(lm, t)), gather_kept(values, Nat.is_eq(lm, t), rm, gather(values, before, Some{0.0}))) 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=List.append 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.add 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=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_fiber_proof.bend&name=kept https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked_split https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=gather https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=gather_append https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=gather_kept https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=offsets_walk https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=succ_add 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=Index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row 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=extents https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_table 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/shape/core.bend&name=walk_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_right 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/pointwise_proof.bend&name=word_exact 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