def core
bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_proofs.bend:389
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend as BinaryProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
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/storage/array.bend as ArrayCore
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
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/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/binary_storage_proof.bend as Owned
import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts
389def core(+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>}, +dl: Nat, +fitsl: {Storage.bounds(dl, U32.to_nat(Shape.count(left))) == True{} : Bool}, -bl: Model.Balanced(F32, dl, Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill)),
390 -fl: {Storage.bounds(dl, U32.to_nat(Shape.count(left))) == True{} : Bool},
391 +dr: Nat, +fitsr: {Storage.bounds(dr, U32.to_nat(Shape.count(right))) == True{} : Bool}, -br: Model.Balanced(F32, dr, Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)),
392 -fr: {Storage.bounds(dr, U32.to_nat(Shape.count(right))) == True{} : Bool},
393 +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool},
394 -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
395 hyp: @-kl: {Lifecycle.logical_length(StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{})) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-kr: {Lifecycle.logical_length(StorageLaws.step(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, StorageLaws.First{})) == 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), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f})) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} -> P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{StorageLaws.step(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, StorageLaws.First{}), kr}}), 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), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), ko}}}))) ->
396 @-lfits: {Lifecycle.logical_length(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> @-rfits: {Lifecycle.logical_length(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
397 @-fo: {U32.to_nat(Shape.count(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} ->
398 P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.Packed{left, Core.TTensor{Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, lfits}}),
399 Elementwise.take(Core.Packed{right, Core.TTensor{Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, rfits}}))):
400 lfits => rfits => fo =>
401 take_owned_lift(left, dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill)), {==}, bl, fl, lfits,
402 t => P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, t, Elementwise.take(Core.Packed{right, Core.TTensor{Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, rfits}}))),
403 kl => take_owned_lift(right, dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), {==}, br, fr, rfits,
404 t => P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, (Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill)))), t)),
405 kr => 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.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, U32.to_nat(Shape.count(Shape.output_shape(plan))), Elementwise.build(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), Elementwise.build_balanced(d, Elementwise.splits(d), operation, plan, U32.to_nat(Shape.count(Shape.output_shape(plan))), 0n, Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill)), f},
406 output_eq(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, dl, fitsl, dr, fitsr, d, fits, f),
407 st => k => P(((Core.Packed{left, Core.TTensor{StorageLaws.step(Storage.Owned{dl, U32.to_nat(Shape.count(left)), Api.arr(Owned.norm(U32.to_nat(Shape.count(left)), left_ops, Nil{}), dl, left_fill), bl, fl}, StorageLaws.First{}), kl}}, Core.Packed{right, Core.TTensor{StorageLaws.step(Storage.Owned{dr, U32.to_nat(Shape.count(right)), Api.arr(Owned.norm(U32.to_nat(Shape.count(right)), right_ops, Nil{}), dr, right_fill), br, fr}, StorageLaws.First{}), kr}}), Done{Core.Packed{Shape.output_shape(plan), Core.TTensor{st, k}}})), hyp(kl, kr))(fo)))