def value_reads

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

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/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise

55def value_reads(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +count: Nat, +shape: Shape.Shape, +fill: F32,
56  +ops: List<&2, StorageLaws.Op>, +index: U32) ->
57  {Replayed.value(shape, fill, List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, count)), index) ==
58    Replayed.value(shape, fill, ops, index) : F32}:
59  Equal.trans(F32,
60    Replayed.value(shape, fill, List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, count)), index),
61    StorageLaws.expected(Pointwise.reads(~P, ~map, plan, count), U32.to_nat(Shape.count(shape)), index, Replayed.value(shape, fill, ops, index)),
62    Replayed.value(shape, fill, ops, index),
63    expected_append(ops, Pointwise.reads(~P, ~map, plan, count), U32.to_nat(Shape.count(shape)), index, fill),
64    expected_reads(~P, ~map, plan, count, U32.to_nat(Shape.count(shape)), index, Replayed.value(shape, fill, ops, index)))