def writes_zero

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

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

95# At or above the count, the writes leave the +0.0 fill.
96def writes_zero(+inner: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
97  +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +output: Shape.Shape, +count: Nat, +index: U32,
98  +above: {Nat.is_le(count, U32.to_nat(index)) == True{} : Bool},
99  +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
100  {Replayed.value(output, 0.0, writes(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, count), index) == 0.0 : F32}:
101  match count:
102    case 0n:
103      {==}
104    case 1n+previous:
105      +history = writes(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous)
106      +word = cell_word(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous)
107      +op = {StorageLaws.Write{U32.from_nat(previous), word} : StorageLaws.Op}
108      Equal.trans(F32, Replayed.value(output, 0.0, Replayed.snoc(history, op), index),
109        StorageLaws.latest(U32.to_nat(Shape.count(output)), op, index, Replayed.value(output, 0.0, history, index)), 0.0,
110        Replayed.expected_snoc(history, op, U32.to_nat(Shape.count(output)), index, 0.0),
111        Equal.trans(F32, StorageLaws.latest(U32.to_nat(Shape.count(output)), op, index, Replayed.value(output, 0.0, history, index)),
112          Replayed.value(output, 0.0, history, index), 0.0,
113          write_skip(output, previous, index, word, Replayed.value(output, 0.0, history, index),
114            Conversion.le_successor_lt(previous, Shape.logical_numel(Shape.dimensions(output)), room),
115            Conversion.le_successor_lt(previous, U32.to_nat(index), above)),
116          writes_zero(inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, output, previous, index,
117            Conversion.le_predecessor(previous, U32.to_nat(index), above),
118            Conversion.le_predecessor(previous, Shape.logical_numel(Shape.dimensions(output)), room))))