def run_last
bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:142
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend as BatchedMatmulPROOF
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
142def run_last(+dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +ls: Nat, +rs: Nat, +lp: Nat, +rp: Nat, -accumulator: F32,
143 pl: Array<F32> & F32, pr: Array<F32> & F32, -read: Read<dl, dr, A, B, lp, rp, pl, pr>) ->
144 Parallel.Fact<StridedRun<1n, dl, dr, A, B, ls, rs, lp, rp, accumulator, Matrix.product_run(0n, ls, rs, lp, rp, accumulator, pl, pr)>>:
145 (kl, x) = pl
146 (kr, y) = pr
147 -ex = {\{Read: ex => ey => left_kept => right_kept => ex} : Read<dl, dr, A, B, lp, rp, (kl, x), (kr, y)> ->
148 {Model.observe(F32, dl, A, Refinement.route(dl, U32.from_nat(lp))) == Some{x} : Maybe<&2, F32>}}(read)
149 -ey = {\{Read: ex => ey => left_kept => right_kept => ey} : Read<dl, dr, A, B, lp, rp, (kl, x), (kr, y)> ->
150 {Model.observe(F32, dr, B, Refinement.route(dr, U32.from_nat(rp))) == Some{y} : Maybe<&2, F32>}}(read)
151 -left_kept = {\{Read: ex => ey => left_kept => right_kept => left_kept} : Read<dl, dr, A, B, lp, rp, (kl, x), (kr, y)> ->
152 {kl == A : Array<F32>}}(read)
153 -right_kept = {\{Read: ex => ey => left_kept => right_kept => right_kept} : Read<dl, dr, A, B, lp, rp, (kl, x), (kr, y)> ->
154 {kr == B : Array<F32>}}(read)
155 run_extend(0n, dl, dr, A, B, ls, rs, lp, rp, accumulator, x, y, ex, ey, (F32.add(accumulator, F32.mul(x, y)), (kl, kr)),
156 Parallel.Fact{StridedRun{Nil{}, Unit{}, {==}, left_kept, right_kept}})