TensorVjpPROOF.second_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 350-399 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=350&end_line=399 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 second product x^T @ g reads, on the transposed copy of x and # the copy of g's first half, are the pairs left_transposed_factors names on x # and g themselves. def second_factors(+row: Nat, +column: Nat, +rows: U32, +inner: U32, +columns: U32, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +plan: Layout.Plan, +output_ops: List<&2, StorageLaws.Op>, +moved: {Contracts.words(Laws.transposed(left, plan), 0.0, output_ops, Shape.logical_numel(Shape.dimensions(Laws.transposed(left, plan)))) == PermuteRecords.permuted_words(left, left_fill, left_ops, Laws.swapped(left), Shape.logical_numel(Shape.dimensions(Laws.transposed(left, plan)))) : List<&2, F32>}, +le: {Shape.dimensions(Laws.transposed(left, plan)) == [rows, inner] : List<&2, U32>}, +row_below: {Nat.is_lt(row, U32.to_nat(rows)) == True{} : Bool}, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +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), Laws.transposed(left, plan), 0.0, output_ops, shape, fill, Replayed.snoc(Replayed.snoc(ops, StorageLaws.First{}), StorageLaws.Second{}), count) == Laws.left_transposed_factors(row, column, U32.to_nat(inner), U32.to_nat(columns), left, left_fill, left_ops, Laws.swapped(left), shape, fill, ops, 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(left) +output = Laws.transposed(left, plan) +position = Nat.add(Nat.mul(row, inner_count), previous) +bound = MatmulProof.cell_below(output, rows, inner, le, row, row_below, previous, Conversion.le_successor_lt(previous, inner_count, room)) +cell = U32.from_nat(Nat.add(Nat.mul(previous, column_count), column)) +front = Replayed.snoc(ops, StorageLaws.First{}) factors_snoc( Contracts.factors(row, column, inner_count, column_count, output, 0.0, output_ops, shape, fill, Replayed.snoc(front, StorageLaws.Second{}), previous), Laws.left_transposed_factors(row, column, inner_count, column_count, left, left_fill, left_ops, axes, shape, fill, ops, previous), Replayed.value(output, 0.0, output_ops, U32.from_nat(position)), Replayed.value(shape, fill, Replayed.snoc(front, StorageLaws.Second{}), cell), Replayed.value(left, left_fill, left_ops, U32.from_nat(Values.permute_source_index(left, axes, position))), Replayed.value(shape, fill, ops, cell), second_factors(row, column, rows, inner, columns, left, left_fill, left_ops, plan, output_ops, moved, le, row_below, shape, fill, ops, previous, Conversion.le_predecessor(previous, inner_count, room)), Equal.trans(F32, Replayed.value(output, 0.0, output_ops, U32.from_nat(position)), Replayed.value(left, left_fill, left_ops, U32.from_nat(Values.permute_source_index(left, axes, U32.to_nat(U32.from_nat(position))))), Replayed.value(left, left_fill, left_ops, U32.from_nat(Values.permute_source_index(left, axes, position))), permuted_at(left, left_fill, left_ops, axes, plan, output_ops, moved, U32.from_nat(position), PointwiseProof.word_inside(position, output, bound)), Equal.cong(Nat, F32, number => Replayed.value(left, left_fill, left_ops, U32.from_nat(Values.permute_source_index(left, axes, number))), U32.to_nat(U32.from_nat(position)), position, PointwiseProof.word_exact(position, output, bound))), Equal.trans(F32, Replayed.value(shape, fill, Replayed.snoc(front, StorageLaws.Second{}), cell), Replayed.value(shape, fill, front, cell), Replayed.value(shape, fill, ops, cell), SumToSizeFoldProof.half_keeps(shape, fill, front, StorageLaws.Second{}, cell, {==}), SumToSizeFoldProof.half_keeps(shape, fill, ops, StorageLaws.First{}, cell, {==}))) Uses (36): 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=left_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/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