MatmulPROOF.dot_loop_status: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
Lines 776-800 of bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&start_line=776&end_line=800

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/math_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as MathProof
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

def dot_loop_status(fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
  +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, a: Core.Tensor<left>, b: Core.Tensor<right>,
  -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
  -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
  -row_inside: {Nat.is_lt(U32.to_nat(row), U32.to_nat(rows)) == True{} : Bool},
  -column_inside: {Nat.is_lt(U32.to_nat(column), U32.to_nat(columns)) == True{} : Bool},
  -bound: Shape.LE(Nat.add(fuel, cursor), U32.to_nat(inner))) ->
  Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32, Matrix.natural_dot(fuel, left, right, a, b, row, column, cursor, accumulator)>:
  match fuel:
    case 0n:
      Totality.Status{{==}}
    case 1n+tail:
      dot_decision_status(tail, left, right, row, column, cursor, accumulator,
        Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), a, b, word_cursor_exact(tail, cursor, inner, bound),
        Coordinates.pair_fits(left, rows, inner, row, U32.from_nat(cursor), le, row_inside,
          %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, word_cursor_exact(tail, cursor, inner, bound)) : {Nat.is_lt(_, U32.to_nat(inner)) == True{} : Bool}
          MathProof.cursor_bounds(tail, cursor, U32.to_nat(inner), bound)),
        Coordinates.pair_fits(right, right_inner, columns, U32.from_nat(cursor), column, re,
          %compatible : {Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), _) == True{} : Bool}
          %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, word_cursor_exact(tail, cursor, inner, bound)) : {Nat.is_lt(_, U32.to_nat(inner)) == True{} : Bool}
          MathProof.cursor_bounds(tail, cursor, U32.to_nat(inner), bound), column_inside),
        a => b => value => dot_loop_status(tail, left, right, rows, inner, right_inner, columns, row, column, 1n+cursor, value,
          a, b, le, re, compatible, row_inside, column_inside,
          %Equal.sym(Nat, Nat.add(tail, 1n+cursor), 1n+Nat.add(tail, cursor), Arith.add_succ(tail, cursor)) : Shape.LE(_, U32.to_nat(inner))
          bound))

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=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=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=pair_fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/math_totality.bend&name=Status
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=natural_dot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=dot_decision_status
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=word_cursor_exact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=cursor_bounds