ReduceReplayedProof.run_arr: 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 603-636 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=603&end_line=636 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/storage/api.bend as Api import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce def run_arr(+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, +h: List<&2, Api.Effect>, +d: Nat, +f: F32) -> {Reduce.strided_run(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator, Array.get(F32, Api.arr(h, d, f), U32.from_nat(Reduce.strided_offset(right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n))))) == Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+fuel, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array}: match fuel: case 0n: +lift = Reduce.single_offset(rest, others, Nat.mod(target, left), 0n) +at = Reduce.strided_offset(right, base, digit, lift) %Equal.sym(Array & F32, Array.get(F32, Api.arr(h, d, f), U32.from_nat(at)), (Api.arr(h, d, f), word_at(h, d, f, at)), got(h, d, f, U32.from_nat(at))) : {Reduce.strided_run(0n, right, base, digit, lift, accumulator, _) == Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array} Equal.sym(F32 & Array, Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, Api.arr(h, d, f)), (F32.add(accumulator, word_at(h, d, f, at)), Api.arr(h, d, f)), step_arr(stride, left, right, rest, extent, others, single, 0n, target, base, digit, accumulator, h, d, f)) case 1n+remaining: +lift = Reduce.single_offset(rest, others, Nat.mod(target, left), 0n) +at = Reduce.strided_offset(right, base, digit, lift) +next = F32.add(accumulator, word_at(h, d, f, at)) %Equal.sym(Array & F32, Array.get(F32, Api.arr(h, d, f), U32.from_nat(at)), (Api.arr(h, d, f), word_at(h, d, f, at)), got(h, d, f, U32.from_nat(at))) : {Reduce.strided_run(1n+remaining, right, base, digit, lift, accumulator, _) == Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, Api.arr(h, d, f)) : F32 & Array} Equal.trans(F32 & Array, Reduce.strided_run(remaining, right, base, 1n+digit, lift, next, Array.get(F32, Api.arr(h, d, f), 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, next, Api.arr(h, d, f)), Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, Api.arr(h, d, f)), run_arr(stride, left, right, rest, extent, others, single, remaining, target, base, 1n+digit, next, h, d, f), Equal.sym(F32 & Array, Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, Api.arr(h, d, f)), Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, next, Api.arr(h, d, f)), step_arr(stride, left, right, rest, extent, others, single, 1n+remaining, target, base, digit, accumulator, h, d, f))) Uses (24): 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_replayed_proof.bend&name=got https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=step_arr https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=word_at 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/storage/api.bend&name=Effect https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr