def writes_value

bendtorch-core@0.1.0.0 · src/tensor/contracts/matmul_parallel_proof.bend:49

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_proof.bend as PointwiseProof

49def writes_value(+inner: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
50  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +output: Shape.Shape, +count: Nat, +index: U32,
51  below: {Nat.is_lt(U32.to_nat(index), count) == True{} : Bool},
52  +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
53  {Replayed.value(output, 0.0, writes(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, count), index) ==
54    cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)) : F32}:
55  match count:
56    case 0n:
57      Empty.absurd({Replayed.value(output, 0.0, Nil{}, index) ==
58        cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)) : F32},
59        Arith.lt_zero(U32.to_nat(index), below))
60    case 1n+previous:
61      PointwiseProof.write_split(output, writes(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous),
62        previous, cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous), index,
63        cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)),
64        below, room,
65        at => Equal.cong(Nat, F32, position => cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, position),
66          previous, U32.to_nat(index), Equal.sym(Nat, U32.to_nat(index), previous, at)),
67        earlier => writes_value(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, output, previous, index, earlier,
68          Conversion.le_predecessor(previous, Shape.logical_numel(Shape.dimensions(output)), room)),
69        Shape.bool_case(Nat.is_eq(U32.to_nat(index), previous)))