ReduceReplayedProof.fiber_eq: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend as ReduceReplayedProof Lines 468-505 of bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&start_line=468&end_line=505 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/storage/arith.bend as Arith import bendtorch-core@0.1.0.0/src/storage/api.bend as Api import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend as Par import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as Fiber import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallel def fiber_eq(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32, +source: Par.Source, +below: {ReduceParallel.all_below(Fiber.visited(rows, extents, fuel, target, base, digit), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> {Reduce.fiber(rows, extents, fuel, target, base, digit, accumulator, Api.arr(h, d, f)) == (rfold(shape, fill, ops, Fiber.visited(rows, extents, fuel, target, base, digit), accumulator), Api.arr(h, d, f)) : F32 & Array}: match rows extents fuel: case Nil{} _ _: leaf_eq(base, accumulator, shape, fill, ops, h, d, f, source, Arith.and_left(Nat.is_lt(base, Shape.logical_numel(Shape.dimensions(shape))), True{}, below), Array.get(F32, Api.arr(h, d, f), U32.from_nat(base)), {==}) case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 0n: {==} case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 1n+remaining: +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest +extents : List<&2, Nat> = extent <> others +inner = Nat.mod(target, left) +offset = Nat.add(base, Nat.mul(right, digit)) +low = Fiber.visited(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner)) +high = Fiber.visited(rows, extents, remaining, target, base, 1n+digit) +bound = Shape.logical_numel(Shape.dimensions(shape)) +value = rfold(shape, fill, ops, low, accumulator) Equal.trans(F32 & Array, Reduce.walk_next(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k), Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f))), Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, value, Api.arr(h, d, f)), (rfold(shape, fill, ops, List.append(&2, Nat, low, high), accumulator), Api.arr(h, d, f)), next_eq(v => k => Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, v, k), Reduce.fiber(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, Api.arr(h, d, f)), value, Api.arr(h, d, f), fiber_eq(rest, others, Reduce.first_span(rest, others), inner, offset, Reduce.first_digit(rest, inner), accumulator, shape, fill, ops, h, d, f, source, below_front(low, high, bound, below))), %Equal.sym(F32, rfold(shape, fill, ops, List.append(&2, Nat, low, high), accumulator), rfold(shape, fill, ops, high, value), rfold_append(shape, fill, ops, low, high, accumulator)) : {Reduce.fiber(rows, extents, remaining, target, base, 1n+digit, value, Api.arr(h, d, f)) == (_, Api.arr(h, d, f)) : F32 & Array} fiber_eq(rows, extents, remaining, target, base, 1n+digit, value, shape, fill, ops, h, d, f, source, below_back(low, high, bound, below))) case Shape.Row{+stride, +left, +right} <> +rest Nil{} _: {==} Uses (37): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get 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=Equal.trans 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=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_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul 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.from_nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=fiber https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=first_digit https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=first_span https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=walk_next https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=visited https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=all_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=below_back https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=below_front https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=leaf_eq https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=next_eq https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=rfold https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=rfold_append 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=Shape 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=logical_numel 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/storage/api.bend&name=Effect https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=Source