def dot_loop_status

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:776

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

776def dot_loop_status(fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
777  +row: U32, +column: U32, +cursor: Nat, +accumulator: F32, a: Core.Tensor<left>, b: Core.Tensor<right>,
778  -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
779  -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
780  -row_inside: {Nat.is_lt(U32.to_nat(row), U32.to_nat(rows)) == True{} : Bool},
781  -column_inside: {Nat.is_lt(U32.to_nat(column), U32.to_nat(columns)) == True{} : Bool},
782  -bound: Shape.LE(Nat.add(fuel, cursor), U32.to_nat(inner))) ->
783  Totality.Status<Matrix.Error, Core.Tensor<left> & Core.Tensor<right> & F32, Matrix.natural_dot(fuel, left, right, a, b, row, column, cursor, accumulator)>:
784  match fuel:
785    case 0n:
786      Totality.Status{{==}}
787    case 1n+tail:
788      dot_decision_status(tail, left, right, row, column, cursor, accumulator,
789        Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), a, b, word_cursor_exact(tail, cursor, inner, bound),
790        Coordinates.pair_fits(left, rows, inner, row, U32.from_nat(cursor), le, row_inside,
791          %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}
792          MathProof.cursor_bounds(tail, cursor, U32.to_nat(inner), bound)),
793        Coordinates.pair_fits(right, right_inner, columns, U32.from_nat(cursor), column, re,
794          %compatible : {Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), _) == True{} : Bool}
795          %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}
796          MathProof.cursor_bounds(tail, cursor, U32.to_nat(inner), bound), column_inside),
797        a => b => value => dot_loop_status(tail, left, right, rows, inner, right_inner, columns, row, column, 1n+cursor, value,
798          a, b, le, re, compatible, row_inside, column_inside,
799          %Equal.sym(Nat, Nat.add(tail, 1n+cursor), 1n+Nat.add(tail, cursor), Arith.add_succ(tail, cursor)) : Shape.LE(_, U32.to_nat(inner))
800          bound))