PermuteValues.words_moved: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/permute_values.bend as PermuteValues Lines 507-533 of bendtorch-core@0.1.0.0/src/tensor/permute_values.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&start_line=507&end_line=533 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/layout.bend as Layout 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/index_map.bend as IndexMap 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 Records import bendtorch-core@0.1.0.0/src/tensor/contracts/words_proof.bend as Words import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts # The words the copy loop writes, in index order, are `permuted_words`. def words_moved(+input: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +axes: List<&2, U32>, +plan: Layout.Plan, +count: Nat, +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}) -> {Contracts.words(Layout.output(input, axes, plan), 0.0, IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), count) == Records.permuted_words(input, fill, ops, axes, count) : List<&2, F32>}: match count: case 0n: {==} case 1n+previous: +output = Layout.output(input, axes, plan) +total = Shape.logical_numel(Shape.dimensions(output)) +request : Request = Request{input, axes} +history = IndexMap.writes(~Request, ~source_of, total, request, input, fill, ops) +below = Conversion.le_successor_lt(previous, total, room) +position = U32.from_nat(previous) Words.snoc_equal(Contracts.words(output, 0.0, history, previous), Records.permuted_words(input, fill, ops, axes, previous), Replayed.value(output, 0.0, history, position), Replayed.value(input, fill, ops, U32.from_nat(Values.permute_source_index(input, axes, previous))), words_moved(input, fill, ops, axes, plan, previous, Conversion.le_predecessor(previous, total, room)), Equal.trans(F32, Replayed.value(output, 0.0, history, position), Replayed.value(input, fill, ops, U32.from_nat(Values.permute_source_index(input, axes, U32.to_nat(position)))), Replayed.value(input, fill, ops, U32.from_nat(Values.permute_source_index(input, axes, previous))), PointwiseProof.writes_value(~Unit, ~IndexMap.keep, ~Request, ~source_of, ~source_of, total, Unit{}, request, input, fill, ops, input, fill, ops, output, position, PointwiseProof.word_inside(previous, output, below), Conversion.le_reflexive(total)), Equal.cong(Nat, F32, number => Replayed.value(input, fill, ops, U32.from_nat(Values.permute_source_index(input, axes, number))), U32.to_nat(position), previous, PointwiseProof.word_exact(previous, output, below)))) Uses (32): 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.is_le 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=Base/base.bend&name=Unit 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=words 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/pointwise_proof.bend&name=writes_value 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/contracts/words_proof.bend&name=snoc_equal https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/index_map.bend&name=keep https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/index_map.bend&name=writes 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=output 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.bend&name=Request https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_values.bend&name=source_of 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_reflexive https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_successor_lt