BinaryProofs.allocated_replayed: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend as BinaryProofs Lines 438-456 of bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&start_line=438&end_line=456 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage 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/elementwise.bend as Elementwise 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.bend as Pointwise import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend as Broadcast import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Contracts import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_LAWS.bend as Laws import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts # The parallel build on two replayed inputs into an output that `Core.new` # allocates: binary_replayed below the planner, which broadcast_to shares. def allocated_replayed(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>}, -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type, h: Laws.BinaryWith(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, P)) -> @-lfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-rfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), Core.new(Shape.output_shape(plan), 0.0))): lfits => rfits => Replayed.new_lift(Shape.output_shape(plan), 0.0, result => P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), result)), fo => Owned.created_lift(Shape.count(Shape.output_shape(plan)), 0.0, Conversion.shape_count_within(Shape.output_shape(plan)), s => ((@+left_kept: List<&2, StorageLaws.Op> -> @left_words: {Contracts.words(left, left_fill, left_kept, Shape.logical_numel(Shape.dimensions(left))) == Contracts.words(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))) : List<&2, F32>} -> @-left_kfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_kept)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @+right_kept: List<&2, StorageLaws.Op> -> @right_words: {Contracts.words(right, right_fill, right_kept, Shape.logical_numel(Shape.dimensions(right))) == Contracts.words(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))) : List<&2, F32>} -> @-right_kfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_kept)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> @-ko: {Lifecycle.logical_length(StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), s)) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_kept), left_kfits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_kept), right_kfits}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), s), ko}}}))) -> @-fo: {Lifecycle.logical_length(s) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(Elementwise.parallel_allocated(operation, plan, Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}), Done{Core.TTensor{s, fo}}))), zero => ho => fo => Facts.storage_shift(Shape.output_shape(plan), StorageLaws.replay(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), Storage.Empty{}), Storage.Empty{}, Owned.replay_empty(Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops)), st => k => P(((Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits}), Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits})), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{st, k}}})), ho(left_ops, {==}, lfits, right_ops, {==}, rfits))(fo), d => fits => f => owned_case(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, lfits, rfits, P, d, fits, f))( left_kept => left_words => left_kfits => right_kept => right_words => right_kfits => ko => h(left_kept, left_words, left_kfits, right_kept, right_words, right_kfits, Pointwise.writes(~Elementwise.Operation, ~Elementwise.scalar, ~Shape.BroadcastPlan, ~Broadcast.left_map, ~Broadcast.right_map, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), words_cells(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Conversion.le_reflexive(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))), ko), fo)) Uses (40): 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=Pair 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=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Error 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=broadcast_checked https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=count 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/shape/core.bend&name=output_shape 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/storage/LAWS.bend&name=replay https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage 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/binary_LAWS.bend&name=BinaryWith https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&name=owned_case https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&name=words_cells https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend&name=created_lift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend&name=replay_empty https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend&name=left_map https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast.bend&name=right_map https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=storage_shift https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend&name=writes https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=new_lift 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=Error 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=new https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=pack https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=parallel_allocated https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=scalar 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/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=shape_count_within