def writes_value

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

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/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
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

216def writes_value(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
217  +count: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
218  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape, +index: U32,
219  below: {Nat.is_lt(U32.to_nat(index), count) == True{} : Bool},
220  +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
221  {Replayed.value(shape, 0.0, Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, count, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), index) ==
222    Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)) : F32}:
223  match count:
224    case 0n:
225      Empty.absurd({Replayed.value(shape, 0.0, Nil{}, index) ==
226        Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)) : F32},
227        Arith.lt_zero(U32.to_nat(index), below))
228    case 1n+previous:
229      write_split(shape, Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, previous, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops),
230        previous, Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), index,
231        Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)),
232        below, room,
233        at => Equal.cong(Nat, F32, position => Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position),
234          previous, U32.to_nat(index), Equal.sym(Nat, U32.to_nat(index), previous, at)),
235        earlier => writes_value(~O, ~f, ~P, ~ia, ~ib, previous, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops,
236          shape, index, earlier, Conversion.le_predecessor(previous, Shape.logical_numel(Shape.dimensions(shape)), room)),
237        Shape.bool_case(Nat.is_eq(U32.to_nat(index), previous)))