def writes_zero

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:113

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

113# At or above the count, the writes leave the +0.0 fill.
114def writes_zero(+plan: Shape.BroadcastPlan, +map: PlanMap(plan), +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +output: Shape.Shape, +count: Nat, +index: U32,
115  +above: {Nat.is_le(count, U32.to_nat(index)) == True{} : Bool},
116  +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(output))) == True{} : Bool}) ->
117  {Replayed.value(output, 0.0, writes(plan, map, shape, fill, ops, count), index) == 0.0 : F32}:
118  match count:
119    case 0n:
120      {==}
121    case 1n+previous:
122      +history = writes(plan, map, shape, fill, ops, previous)
123      +word = cell_word(plan, map, shape, fill, ops, previous)
124      +op = {StorageLaws.Write{U32.from_nat(previous), word} : StorageLaws.Op}
125      Equal.trans(F32, Replayed.value(output, 0.0, Replayed.snoc(history, op), index),
126        StorageLaws.latest(U32.to_nat(Shape.count(output)), op, index, Replayed.value(output, 0.0, history, index)), 0.0,
127        Replayed.expected_snoc(history, op, U32.to_nat(Shape.count(output)), index, 0.0),
128        Equal.trans(F32, StorageLaws.latest(U32.to_nat(Shape.count(output)), op, index, Replayed.value(output, 0.0, history, index)),
129          Replayed.value(output, 0.0, history, index), 0.0,
130          write_skip(output, previous, index, word, Replayed.value(output, 0.0, history, index),
131            Conversion.le_successor_lt(previous, Shape.logical_numel(Shape.dimensions(output)), room),
132            Conversion.le_successor_lt(previous, U32.to_nat(index), above)),
133          writes_zero(plan, map, shape, fill, ops, output, previous, index,
134            Conversion.le_predecessor(previous, U32.to_nat(index), above),
135            Conversion.le_predecessor(previous, Shape.logical_numel(Shape.dimensions(output)), room))))