def made

bendtorch-core@0.1.0.0 · src/tensor/permute_values.bend:161

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/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/index_map.bend as IndexMap
import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteProof
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/read_contract.bend as Reads
import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build
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

161# The copy loop's write history, replayed on the storage `Core.new`
162# allocates, is the build's output on the Second half of the source's clone.
163def made(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +fill: F32, +ops: List<&2, StorageLaws.Op>,
164  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Layout.output(input, axes, plan)))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(Layout.output(input, axes, plan)))) == True{} : Bool},
165  +ds: Nat, +fits_s: {Storage.bounds(ds, U32.to_nat(Shape.count(input))) == True{} : Bool}) ->
166  {StorageLaws.replay(IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Build.build(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)),
167    Build.balanced(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), f} : Storage.Storage}:
168  +count_exact = Reads.count_exact(Layout.output(input, axes, plan))
169  Equal.trans(Storage.Storage, StorageLaws.replay(IndexMap.writes(~Request, ~source_of, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
170    StorageLaws.replay(IndexMap.writes(~Request, ~source_of, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
171    Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Build.build(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), Build.balanced(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), f},
172    Equal.cong(Nat, Storage.Storage, count => StorageLaws.replay(IndexMap.writes(~Request, ~source_of, count, Request{input, axes}, input, fill, ops), Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
173      Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Equal.sym(Nat, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), count_exact)),
174    Equal.trans(Storage.Storage, StorageLaws.replay(IndexMap.writes(~Request, ~source_of, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Request{input, axes}, input, fill, ops), Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
175      Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), PermuteProof.spec(input, axes, fill, ops, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), d, 0n), PermuteProof.spec_balanced(input, axes, fill, ops, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), d, 0n), f},
176      Storage.Owned{d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Build.build(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), Build.balanced(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), f},
177      chain(input, axes, fill, ops, d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), f, fits, Shape.count(Layout.output(input, axes, plan)), Conversion.le_reflexive(U32.to_nat(Shape.count(Layout.output(input, axes, plan)))), U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Conversion.le_reflexive(U32.to_nat(Shape.count(Layout.output(input, axes, plan))))),
178      Owned.owned_eq(d, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), PermuteProof.spec(input, axes, fill, ops, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), d, 0n), Build.build(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)),
179        Equal.sym(Array<F32>, Build.build(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)), PermuteProof.spec(input, axes, fill, ops, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), d, 0n),
180          PermuteProof.build_eq(input, axes, fill, ops, plan, ds, fits_s, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), count_exact, d, Build.splits(d), 0n)),
181        PermuteProof.spec_balanced(input, axes, fill, ops, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), d, 0n), f)(Build.balanced(d, Build.Request{input, axes}, U32.to_nat(Shape.count(Layout.output(input, axes, plan))), Api.arr(Api.Right{} <> Owned.norm(U32.to_nat(Shape.count(input)), ops, Nil{}), ds, fill)))))