TensorVjpPROOF.nt_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 672-780 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=672&end_line=780 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/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/matmul.bend as Matrix import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_proof.bend as MatmulProof import bendtorch-core@0.1.0.0/src/tensor/contracts/product_proof.bend as ProductProof def nt_values(+a: Nat, +b: Nat, +left: Shape.Shape, +right: Shape.Shape, +shape: Shape.Shape, +output: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32, -le: {Shape.dimensions(shape) == [rows, inner] : List<&2, U32>}, -re: {Shape.dimensions(right) == [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, right) == 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>}, +back: Shape.Shape, +back_rows: U32, +back_inner: U32, +back_right_inner: U32, +back_columns: U32, -back_le: {Shape.dimensions(shape) == Matrix.arranged(Matrix.Swapped{}, back_rows, back_inner) : List<&2, U32>}, -back_re: {Shape.dimensions(left) == Matrix.arranged(Matrix.Swapped{}, back_columns, back_right_inner) : 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.product_plan(Matrix.Swapped{}, Matrix.Swapped{}, shape, left) == Done{Matrix.Product{back, back_rows, back_inner, back_right_inner, back_columns, back_le, back_re, back_oe, back_compatible}} : Result<&2, &2, Matrix.Error, Matrix.Product>}, +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}) -> NTGoal(a, b, left, right, shape, Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible}, Matrix.Product{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.MatmulNT{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}})): +first : Matrix.Plan = Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible} +second : Matrix.Product = Matrix.Product{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, right, first, first_planned) +back_facts : ProductProof.ProductFacts = ProductProof.plan_facts(Matrix.Swapped{}, Matrix.Swapped{}, shape, left, second, second_planned) +front_oe = MatmulProof.output_dimensions(shape, right, output, rows, inner, right_inner, columns, front_facts) +back_oe_live = ProductProof.output_dimensions(Matrix.Swapped{}, Matrix.Swapped{}, shape, left, back, back_rows, back_inner, back_right_inner, back_columns, back_facts) -Goal : Backward.Pass -> Type = pass => NTGoal(a, b, left, right, shape, first, 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.nt_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} SumToSizeFoldProof.clone_lift(right, right_fill, right_ops, right_fits, pair => Goal(Backward.nt_second(b, right, x, g, Backward.nt_left(a, left, copy, Core.clone_dynamic_result(right, pair)))), y_fits => flipped_fits => -y_back = {Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, Replayed.snoc(right_ops, StorageLaws.First{})), y_fits}} : Core.Dynamic} Contracts.matmul_replayed(shape, right, first, first_planned, fill, Replayed.snoc(ops, StorageLaws.Second{}), copy_fits, right_fill, Replayed.snoc(right_ops, StorageLaws.Second{}), flipped_fits, result => Goal(Backward.nt_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.nt_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} SumToSizeFoldProof.clone_lift(left, left_fill, left_ops, left_fits, pair => Goal(Backward.nt_fourth(Done{delivered}, y_back, last, Backward.nt_right(b, right, again, Core.clone_dynamic_result(left, pair)))), x_fits => turned_fits => -x_back = {Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, Replayed.snoc(left_ops, StorageLaws.First{})), x_fits}} : Core.Dynamic} Contracts.product_replayed(Matrix.Swapped{}, Matrix.Swapped{}, shape, left, second, second_planned, fill, Replayed.snoc(front, StorageLaws.Second{}), again_fits, left_fill, Replayed.snoc(left_ops, StorageLaws.Second{}), turned_fits, result => Goal(Backward.nt_fourth(Done{delivered}, y_back, last, (x_back, Backward.multiplied(b, right, result)))), again_kept => again_words => again_kept_fits => turned_kept => turned_words => turned_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{}), right, right_fill, Replayed.snoc(right_ops, StorageLaws.Second{}), U32.to_nat(inner)), Contracts.factors(row, column, U32.to_nat(inner), U32.to_nat(columns), shape, fill, ops, right, right_fill, right_ops, U32.to_nat(inner)), front_cells(row, row_below, column, column_below), nt_first_factors(row, column, U32.to_nat(inner), U32.to_nat(columns), shape, fill, ops, right, right_fill, right_ops, 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, back_oe_live, back_ops, back_fits, row, row_below, column, column_below, Contracts.product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{}, U32.to_nat(back_inner), U32.to_nat(back_rows), U32.to_nat(back_columns), shape, fill, Replayed.snoc(front, StorageLaws.Second{}), left, left_fill, Replayed.snoc(left_ops, StorageLaws.Second{}), U32.to_nat(back_inner)), Contracts.product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{}, U32.to_nat(back_inner), U32.to_nat(back_rows), U32.to_nat(back_columns), shape, fill, ops, left, left_fill, left_ops, U32.to_nat(back_inner)), back_cells(row, row_below, column, column_below), nt_second_factors(row, column, U32.to_nat(back_inner), U32.to_nat(back_rows), U32.to_nat(back_columns), shape, fill, ops, left, left_fill, left_ops, U32.to_nat(back_inner)))})))))) Uses (54): 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=multiplied https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=nt_first https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=nt_fourth https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=nt_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=nt_right https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=nt_second https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=nt_third 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_PROOF.bend&name=NTGoal https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=nt_first_factors https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=nt_second_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/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/LAWS.bend&name=product_factors https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend&name=product_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/product_proof.bend&name=ProductFacts https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/product_proof.bend&name=output_dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/product_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/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=Order 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=Product https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=arranged 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=product_plan