ReduceParallelProof.run_fiber: 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 475-515 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=475&end_line=515 import Base import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce # The strided run of a row whose rows below take one digit is the fiber of # that row from the same digit, one more word than the run's fuel. def run_fiber(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>, +single: {Reduce.single_rows(rest, others) == True{} : Bool}, fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32, -array: Array, pair: Array & F32, -read: {pair == Array.get(F32, array, U32.from_nat(Reduce.strided_offset(right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)))) : Array & F32}) -> Generic.Fact<{Reduce.strided_run(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator, pair) == Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+fuel, target, base, digit, accumulator, array) : F32 & Array}>: match fuel pair: case 0n Tuple{kept, word}: Generic.Fact{Equal.sym(F32 & Array, Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, array), (F32.add(accumulator, word), kept), {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, array) == Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 0n, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array})> -> {Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, array) == (F32.add(accumulator, word), kept) : F32 & Array}}( fiber_step(stride, left, right, rest, extent, others, single, 0n, target, base, digit, accumulator, array, kept, word, read)))} case 1n+remaining Tuple{kept, word}: +lift = Reduce.single_offset(rest, others, Nat.mod(target, left), 0n) Generic.Fact{Equal.trans(F32 & Array, Reduce.strided_run(remaining, right, base, 1n+digit, lift, F32.add(accumulator, word), Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))), Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept), Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array), {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.strided_run(remaining, right, base, 1n+digit, lift, F32.add(accumulator, word), Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))) == Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array})> -> {Reduce.strided_run(remaining, right, base, 1n+digit, lift, F32.add(accumulator, word), Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))) == Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array}}( run_fiber(stride, left, right, rest, extent, others, single, remaining, target, base, 1n+digit, F32.add(accumulator, word), kept, Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift))), {==})), Equal.sym(F32 & Array, Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array), Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept), {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array) == Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array})> -> {Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array) == Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array}}( fiber_step(stride, left, right, rest, extent, others, single, 1n+remaining, target, base, digit, accumulator, array, kept, word, read))))} Uses (21): 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=F32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod 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=single_offset https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=single_rows https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=strided_offset https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=strided_run https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=fiber_step 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/tensor/parallel_proofs.bend&name=Fact