MatmulPROOF.logical_dot: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF Lines 1381-1433 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=1381&end_line=1433 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/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/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/elementwise_parallel_proof.bend as Parallel import bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend as MatmulParallel import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndex # The factor pairs the parallel build reads from its copies are the # coordinate reads of the inputs the copies came from. def logical_dot(+fuel: Nat, +left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32, +row: Nat, +column: Nat, +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_below: {Nat.is_lt(row, U32.to_nat(rows)) == True{} : Bool}, +column_below: {Nat.is_lt(column, U32.to_nat(columns)) == True{} : Bool}, -a: Core.Tensor, -b: Core.Tensor, +dl: Nat, +dr: Nat, -cl: Array, -cr: Array, -left_reads: Parallel.SourceReads(Core.Packed{left, a}, dl, cl), -right_reads: Parallel.SourceReads(Core.Packed{right, b}, dr, cr), +cursor: Nat, +steps: {Nat.add(cursor, fuel) == U32.to_nat(inner) : Nat}, values: List<&2, DotFold.Factors>, -arr: MatmulParallel.LogicalArr(fuel, dl, dr, cl, cr, U32.to_nat(inner), U32.to_nat(columns), row, column, cursor, values)) -> Parallel.Fact: match fuel values: case 0n Nil{}: Parallel.Fact{Unit{}} case 1n+tail DotFold.Factors{lv, rv} <> rest: +below = MatrixIndex.cursor_below(cursor, tail, U32.to_nat(inner), steps) +left_at = Matrix.left_index(U32.to_nat(inner), row, cursor) +right_at = Matrix.right_index(U32.to_nat(columns), column, cursor) +left_inside = MatrixIndex.word_inside(Nat.add(Nat.mul(row, U32.to_nat(inner)), cursor), left, MatrixIndex.left_below(U32.to_nat(rows), U32.to_nat(inner), row, row_below, left, left_extents(left, rows, inner, le), cursor, below)) +right_inside = MatrixIndex.word_inside(Nat.add(Nat.mul(cursor, U32.to_nat(columns)), column), right, MatrixIndex.right_below(U32.to_nat(inner), U32.to_nat(columns), column, column_below, right, right_extents(right, inner, right_inner, columns, re, compatible), cursor, below)) Parallel.Fact{{\{MatmulParallel.ArrStep: left_observed => right_observed => remaining => Laws.DotStep{MatrixIndex.word_below(cursor, inner, below), Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(left, a, [U32.from_nat(row), U32.from_nat(cursor)]), Core.checked_observe(left, a, left_at), Some{lv}, coordinate_read(left, a, left_at, Shape.flatten_checked(left, [U32.from_nat(row), U32.from_nat(cursor)]), left_flat(left, rows, inner, row, cursor, le, row_below, below)), Equal.trans(Maybe<&2, F32>, Core.checked_observe(left, a, left_at), Model.observe(F32, dl, cl, Refinement.route(dl, left_at)), Some{lv}, Equal.sym(Maybe<&2, F32>, Model.observe(F32, dl, cl, Refinement.route(dl, left_at)), Core.checked_observe(left, a, left_at), left_reads(left_at)(left_inside)), left_observed)), Equal.trans(Maybe<&2, F32>, Laws.coordinate_observe(right, b, [U32.from_nat(cursor), U32.from_nat(column)]), Core.checked_observe(right, b, right_at), Some{rv}, coordinate_read(right, b, right_at, Shape.flatten_checked(right, [U32.from_nat(cursor), U32.from_nat(column)]), right_flat(right, inner, right_inner, columns, column, cursor, re, compatible, column_below, below)), Equal.trans(Maybe<&2, F32>, Core.checked_observe(right, b, right_at), Model.observe(F32, dr, cr, Refinement.route(dr, right_at)), Some{rv}, Equal.sym(Maybe<&2, F32>, Model.observe(F32, dr, cr, Refinement.route(dr, right_at)), Core.checked_observe(right, b, right_at), right_reads(right_at)(right_inside)), right_observed)), {\{Parallel.Fact: p => p} : Parallel.Fact -> Laws.LogicalDot(tail, left, right, a, b, U32.from_nat(row), U32.from_nat(column), 1n+cursor, rest)}( logical_dot(tail, left, right, rows, inner, right_inner, columns, row, column, le, re, compatible, row_below, column_below, a, b, dl, dr, cl, cr, left_reads, right_reads, 1n+cursor, MatrixIndex.steps_next(cursor, tail, U32.to_nat(inner), steps), rest, remaining))}} : MatmulParallel.ArrStep -> Laws.DotStep}(arr)} case 0n DotFold.Factors{lv, rv} <> rest: Parallel.Fact{Empty.absurd(Laws.LogicalDot(0n, left, right, a, b, U32.from_nat(row), U32.from_nat(column), cursor, DotFold.Factors{lv, rv} <> rest), arr)} case 1n+tail Nil{}: Parallel.Fact{Empty.absurd(Laws.LogicalDot(1n+tail, left, right, a, b, U32.from_nat(row), U32.from_nat(column), cursor, Nil{}), arr)} Uses (45): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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.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=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul 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=Base/base.bend&name=Unit 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=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=flatten_checked 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/core.bend&name=Dynamic 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/core.bend&name=checked_observe 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/elementwise_parallel_proof.bend&name=SourceReads https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=left_index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=right_index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend&name=DotStep https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend&name=LogicalDot https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend&name=coordinate_observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=coordinate_read https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=left_extents https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=left_flat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=right_extents https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=right_flat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend&name=ArrStep https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_parallel_proof.bend&name=LogicalArr https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=cursor_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=left_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=right_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=steps_next https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=word_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend&name=word_inside