def replayed_point

bendtorch-core@0.1.0.0 · src/tensor/contracts/pointwise_proof.bend:445

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/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/contracts/replayed.bend as Replayed

445def replayed_point(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
446  -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
447  inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
448  {Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, index)) ==
449    Some{Replayed.value(shape, fill, ops, index)} : Maybe<&2, F32>}:
450  Equal.trans(Maybe<&2, F32>,
451    Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, index)),
452    Core.read_value(shape, Core.read_flat(shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}, index)),
453    Some{Replayed.value(shape, fill, ops, index)},
454    dynamic_value(shape, Core.read_flat(shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}, index)),
455    Replayed.read_found(shape, fill, ops, fits, index, inside))