BatchedMatmulPROOF.strided_logical: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend as BatchedMatmulPROOF
Lines 476-519 of bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&start_line=476&end_line=519

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

# A run whose reads start at a cell's first terms reads the cell's logical
# factor pairs.
def strided_logical(+fuel: Nat, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +lo: Matrix.Order, +ro: Matrix.Order, +inner: Nat,
  +rows: Nat, +columns: Nat, +l1: Nat, +l2: Nat, +r1: Nat, +r2: Nat, +b1: Nat, +b2: Nat, +row: Nat, +column: Nat, +k: Nat,
  +lp: Nat, +rp: Nat, values: List<&2, DotFold.Factors>,
  -el: {lp == Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, k) : Nat},
  -er: {rp == Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, k) : Nat},
  -strided: Laws.Strided(fuel, dl, dr, A, B, Matrix.stride(lo, rows), Matrix.stride(ro, columns), lp, rp, values)) ->
  Parallel.Fact<Laws.Logical(fuel, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, k, values)>:
  match fuel values:
    case 0n Nil{}:
      Parallel.Fact{Unit{}}
    case 1n+tail DotFold.Factors{lv, rv} <> rest:
      Parallel.Fact{{\{Laws.StridedStep: left_observed => right_observed => remaining =>
        Laws.LogicalStep{
          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)))),
            Model.observe(F32, dl, A, Refinement.route(dl, U32.from_nat(lp))), Some{lv},
            Equal.cong(Nat, Maybe<&2, F32>, x => Model.observe(F32, dl, A, Refinement.route(dl, U32.from_nat(x))),
              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)),
            left_observed),
          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)))),
            Model.observe(F32, dr, B, Refinement.route(dr, U32.from_nat(rp))), Some{rv},
            Equal.cong(Nat, Maybe<&2, F32>, x => Model.observe(F32, dr, B, Refinement.route(dr, U32.from_nat(x))),
              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)),
            right_observed),
          {\{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)> ->
            Laws.Logical(tail, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, 1n+k, rest)}(
            strided_logical(tail, dl, dr, A, B, lo, ro, inner, rows, columns, l1, l2, r1, r2, b1, b2, row, column, 1n+k,
              Nat.add(Matrix.stride(lo, rows), lp), Nat.add(Matrix.stride(ro, columns), rp), rest,
              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)),
                Laws.operand_offset(lo, inner, rows, l1, l2, b1, b2, row, 1n+k),
                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),
                operand_step(lo, inner, rows, l1, l2, b1, b2, row, k)),
              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)),
                Laws.operand_offset(ro, inner, columns, r1, r2, b1, b2, column, 1n+k),
                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),
                operand_step(ro, inner, columns, r1, r2, b1, b2, column, k)),
              remaining))}} :
        Laws.StridedStep<tail, dl, dr, A, B, Matrix.stride(lo, rows), Matrix.stride(ro, columns), lp, rp, lv, rv, rest> ->
        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)}
    case 0n DotFold.Factors{lv, rv} <> rest:
      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)}
    case 1n+tail Nil{}:
      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)}

Uses (24):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=Logical
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=LogicalStep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=Strided
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=StridedStep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=operand_offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=operand_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend&name=Factors
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=Order
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=stride