def run_last

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

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

61# The last term of a run: the reads hold the words of A and B, and both
62# arrays come back.
63def run_last(+dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +inner: Nat, +columns: Nat,
64  +row: Nat, +column: Nat, +cursor: Nat, -accumulator: F32,
65  -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),
66  pl: Array<F32> & F32, -exact_l: {pl == Array.get(F32, la, Matrix.left_index(inner, row, cursor)) : Array<F32> & F32},
67  pr: Array<F32> & F32, -exact_r: {pr == Array.get(F32, ra, Matrix.right_index(columns, column, cursor)) : Array<F32> & F32}) ->
68  Parallel.Fact<DotRun<1n, dl, dr, A, B, inner, columns, row, column, cursor, accumulator, Matrix.product_run(0n, 1n, columns, Nat.add(Nat.mul(row, inner), cursor), Nat.add(Nat.mul(cursor, columns), column), accumulator, pl, pr)>>:
69  (kl, x) = pl
70  (kr, y) = pr
71  -ex = Equal.sym(Maybe<&2, F32>, Some{x}, Model.observe(F32, dl, A, Refinement.route(dl, Matrix.left_index(inner, row, cursor))),
72    {\{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>})> ->
73      {Some{Refinement.second(F32, (kl, x))} == Model.observe(F32, dl, A, Refinement.route(dl, Matrix.left_index(inner, row, cursor))) : Maybe<&2, F32>}}(
74      Parallel.read_value(dl, la, A, Matrix.left_index(inner, row, cursor), (kl, x), exact_l, el, left_valid)))
75  -ey = Equal.sym(Maybe<&2, F32>, Some{y}, Model.observe(F32, dr, B, Refinement.route(dr, Matrix.right_index(columns, column, cursor))),
76    {\{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>})> ->
77      {Some{Refinement.second(F32, (kr, y))} == Model.observe(F32, dr, B, Refinement.route(dr, Matrix.right_index(columns, column, cursor))) : Maybe<&2, F32>}}(
78      Parallel.read_value(dr, ra, B, Matrix.right_index(columns, column, cursor), (kr, y), exact_r, er, right_valid)))
79  -kl_kept = {\{Parallel.Fact: p => p} : Parallel.Fact<({Refinement.first(F32, (kl, x)) == A : Array<F32>})> -> {Refinement.first(F32, (kl, x)) == A : Array<F32>}}(
80    Parallel.read_keeps(dl, la, A, Matrix.left_index(inner, row, cursor), (kl, x), exact_l, el, left_valid))
81  -kr_kept = {\{Parallel.Fact: p => p} : Parallel.Fact<({Refinement.first(F32, (kr, y)) == B : Array<F32>})> -> {Refinement.first(F32, (kr, y)) == B : Array<F32>}}(
82    Parallel.read_keeps(dr, ra, B, Matrix.right_index(columns, column, cursor), (kr, y), exact_r, er, right_valid))
83  dot_extend(0n, dl, dr, A, B, inner, columns, row, column, cursor, accumulator, x, y, ex, ey, (F32.add(accumulator, F32.mul(x, y)), (kl, kr)),
84    Parallel.Fact{DotRun{Nil{}, Unit{}, {==}, kl_kept, kr_kept}})