def fits

bendtorch-core@0.1.0.0 · src/tensor/contracts/replayed.bend:44

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/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads

44def fits(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>) ->
45  {Lifecycle.logical_length(storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}:
46  Equal.trans(Nat, Lifecycle.logical_length(storage(shape, fill, ops)), StorageLaws.size(storage(shape, fill, ops)),
47    Shape.logical_numel(Shape.dimensions(shape)),
48    Equal.sym(Nat, StorageLaws.size(storage(shape, fill, ops)), Lifecycle.logical_length(storage(shape, fill, ops)),
49      Reads.size_is_length(storage(shape, fill, ops))),
50    Equal.trans(Nat, StorageLaws.size(storage(shape, fill, ops)), U32.to_nat(Shape.count(shape)),
51      Shape.logical_numel(Shape.dimensions(shape)),
52      StorageLaws.replay_size(Shape.count(shape), fill, ops, Conversion.shape_count_within(shape)), Reads.count_exact(shape)))