TensorVjpPROOF.first_factors: 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 301-348 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=301&end_line=348 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/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/pointwise_proof.bend as PointwiseProof 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_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/dot_fold.bend as DotFold import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values import bendtorch-core@0.1.0.0/src/tensor/permute_values_records.bend as PermuteRecords import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_proof.bend as MatmulProof # The pairs the first product g @ y^T reads, on the copy of g and the # transposed copy of y, are the pairs right_transposed_factors names on g and # y themselves. def first_factors(+row: Nat, +column: Nat, +inner: U32, +right_inner: U32, +columns: U32, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +plan: Layout.Plan, +output_ops: List<&2, StorageLaws.Op>, +moved: {Contracts.words(Laws.transposed(right, plan), 0.0, output_ops, Shape.logical_numel(Shape.dimensions(Laws.transposed(right, plan)))) == PermuteRecords.permuted_words(right, right_fill, right_ops, Laws.swapped(right), Shape.logical_numel(Shape.dimensions(Laws.transposed(right, plan)))) : List<&2, F32>}, +re: {Shape.dimensions(Laws.transposed(right, plan)) == [right_inner, columns] : List<&2, U32>}, +compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat}, +column_below: {Nat.is_lt(column, U32.to_nat(columns)) == True{} : Bool}, +count: Nat, +room: {Nat.is_le(count, U32.to_nat(inner)) == True{} : Bool}) -> {Contracts.factors(row, column, U32.to_nat(inner), U32.to_nat(columns), shape, fill, Replayed.snoc(ops, StorageLaws.Second{}), Laws.transposed(right, plan), 0.0, output_ops, count) == 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), count) : List<&2, DotFold.Factors>}: match count: case 0n: {==} case 1n+previous: +inner_count = U32.to_nat(inner) +column_count = U32.to_nat(columns) +axes = Laws.swapped(right) +output = Laws.transposed(right, plan) +position = Nat.add(Nat.mul(previous, column_count), column) +below = MatmulProof.lt_bound(previous, inner_count, U32.to_nat(right_inner), compatible, Conversion.le_successor_lt(previous, inner_count, room)) +bound = MatmulProof.cell_below(output, right_inner, columns, re, previous, below, column, column_below) +cell = U32.from_nat(Nat.add(Nat.mul(row, inner_count), previous)) factors_snoc( Contracts.factors(row, column, inner_count, column_count, shape, fill, Replayed.snoc(ops, StorageLaws.Second{}), output, 0.0, output_ops, previous), Laws.right_transposed_factors(row, column, inner_count, column_count, shape, fill, ops, right, right_fill, right_ops, axes, previous), Replayed.value(shape, fill, Replayed.snoc(ops, StorageLaws.Second{}), cell), Replayed.value(output, 0.0, output_ops, U32.from_nat(position)), Replayed.value(shape, fill, ops, cell), Replayed.value(right, right_fill, right_ops, U32.from_nat(Values.permute_source_index(right, axes, position))), first_factors(row, column, inner, right_inner, columns, shape, fill, ops, right, right_fill, right_ops, plan, output_ops, moved, re, compatible, column_below, previous, Conversion.le_predecessor(previous, inner_count, room)), SumToSizeFoldProof.half_keeps(shape, fill, ops, StorageLaws.Second{}, cell, {==}), Equal.trans(F32, Replayed.value(output, 0.0, output_ops, U32.from_nat(position)), Replayed.value(right, right_fill, right_ops, U32.from_nat(Values.permute_source_index(right, axes, U32.to_nat(U32.from_nat(position))))), Replayed.value(right, right_fill, right_ops, U32.from_nat(Values.permute_source_index(right, axes, position))), permuted_at(right, right_fill, right_ops, axes, plan, output_ops, moved, U32.from_nat(position), PointwiseProof.word_inside(position, output, bound)), Equal.cong(Nat, F32, number => Replayed.value(right, right_fill, right_ops, U32.from_nat(Values.permute_source_index(right, axes, number))), U32.to_nat(U32.from_nat(position)), position, PointwiseProof.word_exact(position, output, bound)))) Uses (37): 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=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=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_le 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=bendtorch-core@0.1.0.0/src/autograd/sum_to_size_fold_PROOF.bend&name=half_keeps 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=factors_snoc https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend&name=permuted_at 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=words https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_proof.bend&name=cell_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_proof.bend&name=lt_bound https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend&name=word_exact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend&name=word_inside 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=value 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/layout.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=permute_source_index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values_records.bend&name=permuted_words https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_predecessor https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_successor_lt