def frozen_values
bendtorch-core@0.1.0.0 · src/autograd/tensor_vjp_PROOF.bend:833
import bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend as TensorVjpPROOF
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/product_proof.bend as ProductProof
833def frozen_values(+b: Nat, +left: Shape.Shape, +right: Shape.Shape, +shape: Shape.Shape,
834 +back: Shape.Shape, +back_rows: U32, +back_inner: U32, +back_right_inner: U32, +back_columns: U32,
835 -back_le: {Shape.dimensions(shape) == Matrix.arranged(Matrix.Swapped{}, back_rows, back_inner) : List<&2, U32>},
836 -back_re: {Shape.dimensions(left) == Matrix.arranged(Matrix.Swapped{}, back_columns, back_right_inner) : List<&2, U32>},
837 -back_oe: {Shape.dimensions(back) == [back_rows, back_columns] : List<&2, U32>},
838 -back_compatible: {U32.to_nat(back_inner) == U32.to_nat(back_right_inner) : Nat},
839 +second_planned: {Matrix.product_plan(Matrix.Swapped{}, Matrix.Swapped{}, shape, left) ==
840 Done{Matrix.Product{back, back_rows, back_inner, back_right_inner, back_columns, back_le, back_re, back_oe, back_compatible}} :
841 Result<&2, &2, Matrix.Error, Matrix.Product<Matrix.Swapped{}, Matrix.Swapped{}, shape, left>>},
842 +second_same: {Shape.dimensions(back) == Shape.dimensions(right) : List<&2, U32>},
843 +fill: F32, +ops: List<&2, StorageLaws.Op>,
844 -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
845 +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
846 -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat},
847 +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>,
848 -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}) ->
849 FrozenGoal(b, left, right, shape,
850 Matrix.Product{back, back_rows, back_inner, back_right_inner, back_columns, back_le, back_re, back_oe, back_compatible},
851 fill, ops, left_fill, left_ops,
852 Backward.vjp_matmul_nt_right(b, right,
853 Backward.Operands{Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
854 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}}},
855 Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})):
856 +second : Matrix.Product<Matrix.Swapped{}, Matrix.Swapped{}, shape, left> =
857 Matrix.Product{back, back_rows, back_inner, back_right_inner, back_columns, back_le, back_re, back_oe, back_compatible}
858 +back_facts : ProductProof.ProductFacts<Matrix.Swapped{}, Matrix.Swapped{}, shape, left, back, back_rows, back_inner, back_right_inner, back_columns> =
859 ProductProof.plan_facts(Matrix.Swapped{}, Matrix.Swapped{}, shape, left, second, second_planned)
860 +back_oe_live = ProductProof.output_dimensions(Matrix.Swapped{}, Matrix.Swapped{}, shape, left, back, back_rows, back_inner, back_right_inner,
861 back_columns, back_facts)
862 -Goal : Backward.Pass -> Type = pass => FrozenGoal(b, left, right, shape, second, fill, ops, left_fill, left_ops, pass)
863 -x = {Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}} : Core.Dynamic}
864 -y = {Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}} : Core.Dynamic}
865 SumToSizeFoldProof.clone_lift(shape, fill, ops, fits,
866 pair => Goal(Backward.nt_alone_first(b, right, x, y, Core.clone_dynamic_result(shape, pair))),
867 g_fits => copy_fits =>
868 -g = {Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, Replayed.snoc(ops, StorageLaws.First{})), g_fits}} : Core.Dynamic}
869 -copy = {Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, Replayed.snoc(ops, StorageLaws.Second{})), copy_fits}} : Core.Dynamic}
870 SumToSizeFoldProof.clone_lift(left, left_fill, left_ops, left_fits,
871 pair => Goal(Backward.nt_alone_second(y, g, Backward.nt_right(b, right, copy, Core.clone_dynamic_result(left, pair)))),
872 x_fits => turned_fits =>
873 -x_back = {Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, Replayed.snoc(left_ops, StorageLaws.First{})), x_fits}} :
874 Core.Dynamic}
875 Contracts.product_replayed(Matrix.Swapped{}, Matrix.Swapped{}, shape, left, second, second_planned,
876 fill, Replayed.snoc(ops, StorageLaws.Second{}), copy_fits,
877 left_fill, Replayed.snoc(left_ops, StorageLaws.Second{}), turned_fits,
878 result => Goal(Backward.nt_alone_second(y, g, (x_back, Backward.multiplied(b, right, result)))),
879 again_kept => again_words => again_kept_fits => turned_kept => turned_words => turned_kept_fits =>
880 back_ops => back_cells => back_fits =>
881 Laws.MatmulSoleContract{
882 {==},
883 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, dimensions => Some{dimensions},
884 Shape.dimensions(back), Shape.dimensions(right), second_same),
885 row => row_below => column => column_below =>
886 +row_below = row_below
887 +column_below = column_below
888 product_cell(back, back_rows, back_columns, back_oe_live, back_ops, back_fits, row, row_below, column, column_below,
889 Contracts.product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{}, U32.to_nat(back_inner),
890 U32.to_nat(back_rows), U32.to_nat(back_columns), shape, fill, Replayed.snoc(ops, StorageLaws.Second{}),
891 left, left_fill, Replayed.snoc(left_ops, StorageLaws.Second{}), U32.to_nat(back_inner)),
892 Contracts.product_factors(row, column, Matrix.Swapped{}, Matrix.Swapped{}, U32.to_nat(back_inner),
893 U32.to_nat(back_rows), U32.to_nat(back_columns), shape, fill, ops, left, left_fill, left_ops, U32.to_nat(back_inner)),
894 back_cells(row, row_below, column, column_below),
895 frozen_factors(row, column, U32.to_nat(back_inner), U32.to_nat(back_rows), U32.to_nat(back_columns),
896 shape, fill, ops, left, left_fill, left_ops, U32.to_nat(back_inner)))})))