TensorVjpPROOF.matmul_values: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend as TensorVjpPROOF Lines 462-579 of bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&start_line=462&end_line=579 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts import bendtorch-core@0.1.0.0/src/autograd/sum_to_size_fold_PROOF.bend as SumToSizeFoldProof import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward import bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_LAWS.bend as Laws import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose import bendtorch-core@0.1.0.0/src/tensor/permute_values_contract_LAWS.bend as PermuteLaws import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_proof.bend as MatmulProof def matmul_values(+a: Nat, +b: Nat, +left: Shape.Shape, +right: Shape.Shape, +shape: Shape.Shape, +right_inside: {True{} == Transpose.valid(right, 0, 1) : Bool}, +right_plan: Layout.Plan, +right_laid: {Layout.permutation(right, Laws.swapped(right)) == Done{right_plan} : Result<&2, &2, Layout.Error, Layout.Plan>}, +output: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32, -le: {Shape.dimensions(shape) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(Laws.transposed(right, right_plan)) == [right_inner, columns] : List<&2, U32>}, -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>}, -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat}, +first_planned: {Matrix.plan(shape, Laws.transposed(right, right_plan)) == Done{Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible}} : Result<&2, &2, Matrix.Error, Matrix.Plan>}, +first_same: {Shape.dimensions(output) == Shape.dimensions(left) : List<&2, U32>}, +left_inside: {True{} == Transpose.valid(left, 0, 1) : Bool}, +left_plan: Layout.Plan, +left_laid: {Layout.permutation(left, Laws.swapped(left)) == Done{left_plan} : Result<&2, &2, Layout.Error, Layout.Plan>}, +back: Shape.Shape, +back_rows: U32, +back_inner: U32, +back_right_inner: U32, +back_columns: U32, -back_le: {Shape.dimensions(Laws.transposed(left, left_plan)) == [back_rows, back_inner] : List<&2, U32>}, -back_re: {Shape.dimensions(shape) == [back_right_inner, back_columns] : List<&2, U32>}, -back_oe: {Shape.dimensions(back) == [back_rows, back_columns] : List<&2, U32>}, -back_compatible: {U32.to_nat(back_inner) == U32.to_nat(back_right_inner) : Nat}, +second_planned: {Matrix.plan(Laws.transposed(left, left_plan), shape) == Done{Matrix.Plan{back, back_rows, back_inner, back_right_inner, back_columns, back_le, back_re, back_oe, back_compatible}} : Result<&2, &2, Matrix.Error, Matrix.Plan>}, +second_same: {Shape.dimensions(back) == Shape.dimensions(right) : List<&2, U32>}, +fill: F32, +ops: List<&2, StorageLaws.Op>, -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat}, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}) -> MatmulGoal(a, b, left, right, shape, right_plan, Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible}, left_plan, Matrix.Plan{back, back_rows, back_inner, back_right_inner, back_columns, back_le, back_re, back_oe, back_compatible}, fill, ops, left_fill, left_ops, right_fill, right_ops, Backward.vjp(Backward.Matmul{a, b, left, right}, Backward.Operands{Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}}}, Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})): +flipped = Laws.transposed(right, right_plan) +turned = Laws.transposed(left, left_plan) +first : Matrix.Plan = Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible} +second : Matrix.Plan = Matrix.Plan{back, back_rows, back_inner, back_right_inner, back_columns, back_le, back_re, back_oe, back_compatible} +front_facts : MatmulProof.MatrixFacts = MatmulProof.plan_facts(shape, flipped, first, first_planned) +back_facts : MatmulProof.MatrixFacts = MatmulProof.plan_facts(turned, shape, second, second_planned) +front_re = facts_right(shape, flipped, output, rows, inner, right_inner, columns, front_facts) +front_oe = MatmulProof.output_dimensions(shape, flipped, output, rows, inner, right_inner, columns, front_facts) +front_compatible = facts_compatible(shape, flipped, output, rows, inner, right_inner, columns, front_facts) +turned_le = facts_left(turned, shape, back, back_rows, back_inner, back_right_inner, back_columns, back_facts) +turned_oe = MatmulProof.output_dimensions(turned, shape, back, back_rows, back_inner, back_right_inner, back_columns, back_facts) -Goal : Backward.Pass -> Type = pass => MatmulGoal(a, b, left, right, shape, right_plan, first, left_plan, second, fill, ops, left_fill, left_ops, right_fill, right_ops, pass) -x = {Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}} : Core.Dynamic} -y = {Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}} : Core.Dynamic} +front = Replayed.snoc(ops, StorageLaws.First{}) SumToSizeFoldProof.clone_lift(shape, fill, ops, fits, pair => Goal(Backward.matmul_first(a, b, left, right, x, y, Core.clone_dynamic_result(shape, pair))), g_fits => copy_fits => -g = {Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, front), g_fits}} : Core.Dynamic} -copy = {Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, Replayed.snoc(ops, StorageLaws.Second{})), copy_fits}} : Core.Dynamic} PermuteLaws.transpose_replayed(right, right_fill, right_ops, right_fits, 0, 1, right_inside, right_plan, right_laid, pair => Goal(Backward.matmul_second(b, right, x, g, Backward.left_product(a, left, copy, pair))), y_kept => y_words => y_fits => flipped_ops => flipped_moved => flipped_fits => -y_back = {Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, y_kept), y_fits}} : Core.Dynamic} Contracts.matmul_replayed(shape, flipped, first, first_planned, fill, Replayed.snoc(ops, StorageLaws.Second{}), copy_fits, 0.0, flipped_ops, flipped_fits, result => Goal(Backward.matmul_second(b, right, x, g, (y_back, Backward.multiplied(a, left, result)))), copy_kept => copy_words => copy_kept_fits => flipped_kept => flipped_words => flipped_kept_fits => output_ops => front_cells => output_fits => -delivered = {Backward.Contribution{a, left, Core.Packed{output, Core.TTensor{Replayed.storage(output, 0.0, output_ops), output_fits}}} : Backward.Contribution} SumToSizeFoldProof.clone_lift(shape, fill, front, g_fits, pair => Goal(Backward.matmul_third(b, right, Done{delivered}, y_back, x, Core.clone_dynamic_result(shape, pair))), last_fits => again_fits => -last = {Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, Replayed.snoc(front, StorageLaws.First{})), last_fits}} : Core.Dynamic} -again = {Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, Replayed.snoc(front, StorageLaws.Second{})), again_fits}} : Core.Dynamic} PermuteLaws.transpose_replayed(left, left_fill, left_ops, left_fits, 0, 1, left_inside, left_plan, left_laid, pair => Goal(Backward.matmul_fourth(Done{delivered}, y_back, last, Backward.right_product(b, right, again, pair))), x_kept => x_words => x_fits => turned_ops => turned_moved => turned_fits => -x_back = {Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, x_kept), x_fits}} : Core.Dynamic} Contracts.matmul_replayed(turned, shape, second, second_planned, 0.0, turned_ops, turned_fits, fill, Replayed.snoc(front, StorageLaws.Second{}), again_fits, result => Goal(Backward.matmul_fourth(Done{delivered}, y_back, last, (x_back, Backward.multiplied(b, right, result)))), turned_kept => turned_words => turned_kept_fits => again_kept => again_words => again_kept_fits => back_ops => back_cells => back_fits => Laws.MatmulPairContract{ {==}, Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, dimensions => Some{dimensions}, Shape.dimensions(output), Shape.dimensions(left), first_same), row => row_below => column => column_below => +row_below = row_below +column_below = column_below product_cell(output, rows, columns, front_oe, output_ops, output_fits, row, row_below, column, column_below, Contracts.factors(row, column, U32.to_nat(inner), U32.to_nat(columns), shape, fill, Replayed.snoc(ops, StorageLaws.Second{}), flipped, 0.0, flipped_ops, U32.to_nat(inner)), Laws.right_transposed_factors(row, column, U32.to_nat(inner), U32.to_nat(columns), shape, fill, ops, right, right_fill, right_ops, Laws.swapped(right), U32.to_nat(inner)), front_cells(row, row_below, column, column_below), first_factors(row, column, inner, right_inner, columns, shape, fill, ops, right, right_fill, right_ops, right_plan, flipped_ops, flipped_moved, front_re, front_compatible, column_below, U32.to_nat(inner), Conversion.le_reflexive(U32.to_nat(inner)))), {==}, Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, dimensions => Some{dimensions}, Shape.dimensions(back), Shape.dimensions(right), second_same), row => row_below => column => column_below => +row_below = row_below +column_below = column_below product_cell(back, back_rows, back_columns, turned_oe, back_ops, back_fits, row, row_below, column, column_below, Contracts.factors(row, column, U32.to_nat(back_inner), U32.to_nat(back_columns), turned, 0.0, turned_ops, shape, fill, Replayed.snoc(front, StorageLaws.Second{}), U32.to_nat(back_inner)), Laws.left_transposed_factors(row, column, U32.to_nat(back_inner), U32.to_nat(back_columns), left, left_fill, left_ops, Laws.swapped(left), shape, fill, ops, U32.to_nat(back_inner)), back_cells(row, row_below, column, column_below), second_factors(row, column, back_rows, back_inner, back_columns, left, left_fill, left_ops, left_plan, turned_ops, turned_moved, turned_le, row_below, shape, fill, ops, U32.to_nat(back_inner), Conversion.le_reflexive(U32.to_nat(back_inner))))})))))) Uses (59): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong 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=Result https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 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/autograd/sum_to_size_fold_PROOF.bend&name=clone_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Contribution https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Node https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Pass https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Saved https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=left_product https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=matmul_first https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=matmul_fourth https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=matmul_second https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=matmul_third https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=multiplied https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=right_product https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=vjp https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_LAWS.bend&name=MatmulPairContract https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_LAWS.bend&name=left_transposed_factors https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_LAWS.bend&name=right_transposed_factors https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_LAWS.bend&name=swapped https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_LAWS.bend&name=transposed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=MatmulGoal https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=facts_compatible https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=facts_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=facts_right https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=first_factors https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=product_cell https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=second_factors 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=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&name=factors https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&name=matmul_replayed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_proof.bend&name=MatrixFacts https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_proof.bend&name=output_dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_proof.bend&name=plan_facts https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=snoc https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=storage 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=clone_dynamic_result https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Error https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=permutation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=logical_length 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=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values_contract_LAWS.bend&name=transpose_replayed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend&name=valid https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_reflexive