def strided_logical

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:476

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/batched_matmul_LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel

476# A run whose reads start at a cell's first terms reads the cell's logical
477# factor pairs.
478def strided_logical(+fuel: Nat, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +lo: Matrix.Order, +ro: Matrix.Order, +inner: Nat,
479  +rows: Nat, +columns: Nat, +l1: Nat, +l2: Nat, +r1: Nat, +r2: Nat, +b1: Nat, +b2: Nat, +row: Nat, +column: Nat, +k: Nat,
480  +lp: Nat, +rp: Nat, values: List<&2, DotFold.Factors>,
481  -el: {lp == Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, k) : Nat},
482  -er: {rp == Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, k) : Nat},
483  -strided: Laws.Strided(fuel, dl, dr, A, B, Matrix.stride(lo, rows), Matrix.stride(ro, columns), lp, rp, values)) ->
484  Parallel.Fact<Laws.Logical(fuel, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, k, values)>:
485  match fuel values:
486    case 0n Nil{}:
487      Parallel.Fact{Unit{}}
488    case 1n+tail DotFold.Factors{lv, rv} <> rest:
489      Parallel.Fact{{\{Laws.StridedStep: left_observed => right_observed => remaining =>
490        Laws.LogicalStep{
491          Equal.trans(Maybe<&2, F32>, Model.observe(F32, dl, A, Refinement.route(dl, U32.from_nat(Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, k)))),
492            Model.observe(F32, dl, A, Refinement.route(dl, U32.from_nat(lp))), Some{lv},
493            Equal.cong(Nat, Maybe<&2, F32>, x => Model.observe(F32, dl, A, Refinement.route(dl, U32.from_nat(x))),
494              Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, k), lp, Equal.sym(Nat, lp, Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, k), el)),
495            left_observed),
496          Equal.trans(Maybe<&2, F32>, Model.observe(F32, dr, B, Refinement.route(dr, U32.from_nat(Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, k)))),
497            Model.observe(F32, dr, B, Refinement.route(dr, U32.from_nat(rp))), Some{rv},
498            Equal.cong(Nat, Maybe<&2, F32>, x => Model.observe(F32, dr, B, Refinement.route(dr, U32.from_nat(x))),
499              Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, k), rp, Equal.sym(Nat, rp, Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, k), er)),
500            right_observed),
501          {\{Parallel.Fact: p => p} : Parallel.Fact<Laws.Logical(tail, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, 1n+k, rest)> ->
502            Laws.Logical(tail, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, 1n+k, rest)}(
503            strided_logical(tail, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, 1n+k,
504              Nat.add(Matrix.stride(lo, rows), lp), Nat.add(Matrix.stride(ro, columns), rp), rest,
505              Equal.trans(Nat, Nat.add(Matrix.stride(lo, rows), lp), Nat.add(Matrix.stride(lo, rows), Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, k)),
506                Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 1n+k),
507                Equal.cong(Nat, Nat, x => Nat.add(Matrix.stride(lo, rows), x), lp, Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, k), el),
508                operand_step(lo, inner, rows, l1, l2, b1, b2, row, k)),
509              Equal.trans(Nat, Nat.add(Matrix.stride(ro, columns), rp), Nat.add(Matrix.stride(ro, columns), Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, k)),
510                Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 1n+k),
511                Equal.cong(Nat, Nat, x => Nat.add(Matrix.stride(ro, columns), x), rp, Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, k), er),
512                operand_step(ro, inner, columns, r1, r2, b1, b2, column, k)),
513              remaining))}} :
514        Laws.StridedStep<tail, dl, dr, A, B, Matrix.stride(lo, rows), Matrix.stride(ro, columns), lp, rp, lv, rv, rest> ->
515        Laws.LogicalStep<tail, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, k, lv, rv, rest>}(strided)}
516    case 0n DotFold.Factors{lv, rv} <> rest:
517      Parallel.Fact{Empty.absurd(Laws.Logical(0n, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, k, DotFold.Factors{lv, rv} <> rest), strided)}
518    case 1n+tail Nil{}:
519      Parallel.Fact{Empty.absurd(Laws.Logical(1n+tail, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, k, Nil{}), strided)}