def run_fiber

bendtorch-core@0.1.0.0 · src/autograd/reduce_parallel_proof.bend:475

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

475# The strided run of a row whose rows below take one digit is the fiber of
476# that row from the same digit, one more word than the run's fuel.
477def run_fiber(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
478  +single: {Reduce.single_rows(rest, others) == True{} : Bool}, fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
479  -array: Array<F32>, pair: Array<F32> & F32,
480  -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> & F32}) ->
481  Generic.Fact<{Reduce.strided_run(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator, pair) ==
482    Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+fuel, target, base, digit, accumulator, array) : F32 & Array<F32>}>:
483  match fuel pair:
484    case 0n Tuple{kept, word}:
485      Generic.Fact{Equal.sym(F32 & Array<F32>,
486        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, array),
487        (F32.add(accumulator, word), kept),
488        {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, array) ==
489          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 0n, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>})> ->
490          {Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n, target, base, digit, accumulator, array) ==
491            (F32.add(accumulator, word), kept) : F32 & Array<F32>}}(
492          fiber_step(stride, left, right, rest, extent, others, single, 0n, target, base, digit, accumulator, array, kept, word, read)))}
493    case 1n+remaining Tuple{kept, word}:
494      +lift = Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)
495      Generic.Fact{Equal.trans(F32 & Array<F32>,
496        Reduce.strided_run(remaining, right, base, 1n+digit, lift, F32.add(accumulator, word),
497          Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))),
498        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept),
499        Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array),
500        {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.strided_run(remaining, right, base, 1n+digit, lift, F32.add(accumulator, word),
501          Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))) ==
502          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>})> ->
503          {Reduce.strided_run(remaining, right, base, 1n+digit, lift, F32.add(accumulator, word),
504            Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift)))) ==
505            Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>}}(
506          run_fiber(stride, left, right, rest, extent, others, single, remaining, target, base, 1n+digit, F32.add(accumulator, word), kept,
507            Array.get(F32, kept, U32.from_nat(Reduce.strided_offset(right, base, 1n+digit, lift))), {==})),
508        Equal.sym(F32 & Array<F32>,
509          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array),
510          Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept),
511          {\{Generic.Fact: p => p} : Generic.Fact<({Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array) ==
512            Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>})> ->
513            {Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 2n+remaining, target, base, digit, accumulator, array) ==
514              Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, 1n+remaining, target, base, 1n+digit, F32.add(accumulator, word), kept) : F32 & Array<F32>}}(
515            fiber_step(stride, left, right, rest, extent, others, single, 1n+remaining, target, base, digit, accumulator, array, kept, word, read))))}