def owned_case

bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_proofs.bend:409

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/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/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_storage_proof.bend as Owned
import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts

409# The output storage is owned: normalize the left input, then the right one,
410# and run `core`.
411def owned_case(+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>}, -lfits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat},
412  -rfits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat},
413  -P: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
414  +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}) ->
415  (@+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), 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{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), 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}}}))) -> @-fo: {U32.to_nat(Shape.count(Shape.output_shape(plan))) == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat} ->
416  P(Elementwise.parallel_output(operation, plan, d, U32.to_nat(Shape.count(Shape.output_shape(plan))), f, fo, Elementwise.take(Core.pack(left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), lfits})), Elementwise.take(Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits})))):
417  ho => fo =>
418    Facts.input_lift(left, left_fill, left_ops, left_positive(left, right, plan, planned, d, fits),
419      sl => (@-lf: {Lifecycle.logical_length(sl) == Shape.logical_numel(Shape.dimensions(left)) : Nat} -> (@-kl: {Lifecycle.logical_length(StorageLaws.step(sl, StorageLaws.First{})) == 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), 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(sl, StorageLaws.First{}), kl}}, 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), 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}}}))) ->
420        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{sl, lf}}), Elementwise.take(Core.pack(right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), rfits}))))),
421      dl => fitsl => bl => fl => lf => hl =>
422        Facts.input_lift(right, right_fill, right_ops, right_positive(left, right, plan, planned, d, fits),
423          sr => (@-rf: {Lifecycle.logical_length(sr) == Shape.logical_numel(Shape.dimensions(right)) : Nat} -> (@-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(sr, 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(sr, 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}}}))) ->
424            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}, lf}}),
425              Elementwise.take(Core.Packed{right, Core.TTensor{sr, rf}})))),
426          dr => fitsr => br => fr => rf => hr => core(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, planned, dl, fitsl, bl, fl, dr, fitsr, br, fr, d, fits, f, P, hr)(lf, rf, fo))(
427          rfits,
428          kl => Facts.storage_shift(right, Replayed.storage(right, right_fill, Replayed.snoc(right_ops, StorageLaws.First{})),
429            StorageLaws.step(Replayed.storage(right, right_fill, right_ops), StorageLaws.First{}), Replayed.replay_snoc(right_ops, StorageLaws.First{}, right, right_fill),
430            st => k => (@-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{st, k}}), 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}}}))),
431            rk => hl(kl, Replayed.snoc(right_ops, StorageLaws.First{}), words_first(right, right_fill, right_ops, Shape.logical_numel(Shape.dimensions(right))), rk))))(
432      lfits,
433      Facts.storage_shift(left, Replayed.storage(left, left_fill, Replayed.snoc(left_ops, StorageLaws.First{})),
434        StorageLaws.step(Replayed.storage(left, left_fill, left_ops), StorageLaws.First{}), Replayed.replay_snoc(left_ops, StorageLaws.First{}, left, left_fill),
435        st => k => (@+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), 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{st, k}}, 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), 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}}}))),
436        lk => ho(Replayed.snoc(left_ops, StorageLaws.First{}), words_first(left, left_fill, left_ops, Shape.logical_numel(Shape.dimensions(left))), lk)))