def run_next

bendtorch-core@0.1.0.0 · src/tensor/matmul_parallel_proof.bend:97

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel

97# A term with more after it: its reads hold the words of A and B, and the
98# run goes on from the next term's reads of the arrays they hand back.
99def run_next(+rest: Nat, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +inner: Nat, +columns: Nat,
100  +row: Nat, +column: Nat, +cursor: Nat, -accumulator: F32,
101  -la: Array<F32>, -ra: Array<F32>, -el: {la == A : Array<F32>}, -er: {ra == B : Array<F32>}, -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B),
102  pl: Array<F32> & F32, -exact_l: {pl == Array.get(F32, la, Matrix.left_index(inner, row, cursor)) : Array<F32> & F32},
103  pr: Array<F32> & F32, -exact_r: {pr == Array.get(F32, ra, Matrix.right_index(columns, column, cursor)) : Array<F32> & F32},
104  -next: @value: F32 -> @-l: Array<F32> -> @-r: Array<F32> -> @-el: {l == A : Array<F32>} -> @-er: {r == B : Array<F32>} ->
105    Parallel.Fact<DotRun<1n+rest, dl, dr, A, B, inner, columns, row, column, 1n+cursor, value, Matrix.product_run(rest, 1n, columns, Nat.add(Nat.mul(row, inner), 1n+cursor), Nat.add(Nat.mul(1n+cursor, columns), column), value, Array.get(F32, l, Matrix.left_index(inner, row, 1n+cursor)), Array.get(F32, r, Matrix.right_index(columns, column, 1n+cursor)))>>) ->
106  Parallel.Fact<DotRun<2n+rest, dl, dr, A, B, inner, columns, row, column, cursor, accumulator, Matrix.product_run(1n+rest, 1n, columns, Nat.add(Nat.mul(row, inner), cursor), Nat.add(Nat.mul(cursor, columns), column), accumulator, pl, pr)>>:
107  (kl, x) = pl
108  (kr, y) = pr
109  -ex = Equal.sym(Maybe<&2, F32>, Some{x}, Model.observe(F32, dl, A, Refinement.route(dl, Matrix.left_index(inner, row, cursor))),
110    {\{Parallel.Fact: p => p} : Parallel.Fact<({Some{Refinement.second(F32, (kl, x))} == Model.observe(F32, dl, A, Refinement.route(dl, Matrix.left_index(inner, row, cursor))) : Maybe<&2, F32>})> ->
111      {Some{Refinement.second(F32, (kl, x))} == Model.observe(F32, dl, A, Refinement.route(dl, Matrix.left_index(inner, row, cursor))) : Maybe<&2, F32>}}(
112      Parallel.read_value(dl, la, A, Matrix.left_index(inner, row, cursor), (kl, x), exact_l, el, left_valid)))
113  -ey = Equal.sym(Maybe<&2, F32>, Some{y}, Model.observe(F32, dr, B, Refinement.route(dr, Matrix.right_index(columns, column, cursor))),
114    {\{Parallel.Fact: p => p} : Parallel.Fact<({Some{Refinement.second(F32, (kr, y))} == Model.observe(F32, dr, B, Refinement.route(dr, Matrix.right_index(columns, column, cursor))) : Maybe<&2, F32>})> ->
115      {Some{Refinement.second(F32, (kr, y))} == Model.observe(F32, dr, B, Refinement.route(dr, Matrix.right_index(columns, column, cursor))) : Maybe<&2, F32>}}(
116      Parallel.read_value(dr, ra, B, Matrix.right_index(columns, column, cursor), (kr, y), exact_r, er, right_valid)))
117  -kl_kept = {\{Parallel.Fact: p => p} : Parallel.Fact<({Refinement.first(F32, (kl, x)) == A : Array<F32>})> -> {Refinement.first(F32, (kl, x)) == A : Array<F32>}}(
118    Parallel.read_keeps(dl, la, A, Matrix.left_index(inner, row, cursor), (kl, x), exact_l, el, left_valid))
119  -kr_kept = {\{Parallel.Fact: p => p} : Parallel.Fact<({Refinement.first(F32, (kr, y)) == B : Array<F32>})> -> {Refinement.first(F32, (kr, y)) == B : Array<F32>}}(
120    Parallel.read_keeps(dr, ra, B, Matrix.right_index(columns, column, cursor), (kr, y), exact_r, er, right_valid))
121  dot_extend(1n+rest, dl, dr, A, B, inner, columns, row, column, cursor, accumulator, x, y, ex, ey,
122    Matrix.product_run(rest, 1n, columns, Nat.add(1n, Nat.add(Nat.mul(row, inner), cursor)), Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column)), F32.add(accumulator, F32.mul(x, y)), Array.get(F32, kl, U32.from_nat(Nat.add(1n, Nat.add(Nat.mul(row, inner), cursor)))), Array.get(F32, kr, U32.from_nat(Nat.add(columns, Nat.add(Nat.mul(cursor, columns), column))))),
123    run_stepped(rest, dl, dr, A, B, inner, columns, row, column, cursor, F32.add(accumulator, F32.mul(x, y)), kl, kr, next(F32.add(accumulator, F32.mul(x, y)))(kl)(kr)(kl_kept)(kr_kept)))