def write_split

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

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/lifecycle.bend as Lifecycle
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

183# One write appended to a history: index `previous` now holds `written`, and
184# every earlier index keeps the word the history gave it.
185def write_split(+shape: Shape.Shape, +history: List<&2, StorageLaws.Op>, +previous: Nat, +written: F32, +index: U32, +target: F32,
186  below: {Nat.is_lt(U32.to_nat(index), 1n+previous) == True{} : Bool},
187  +room: {Nat.is_le(1n+previous, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
188  hit: @at: {U32.to_nat(index) == previous : Nat} -> {written == target : F32},
189  rec: @earlier: {Nat.is_lt(U32.to_nat(index), previous) == True{} : Bool} -> {Replayed.value(shape, 0.0, history, index) == target : F32},
190  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), previous)>) ->
191  {Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index) == target : F32}:
192  match decision:
193    case Shape.BTrue{same}:
194      +old = Replayed.value(shape, 0.0, history, index)
195      +step = Replayed.expected_snoc(history, StorageLaws.Write{U32.from_nat(previous), written}, U32.to_nat(Shape.count(shape)), index, 0.0)
196      +inside = Conversion.le_successor_lt(previous, Shape.logical_numel(Shape.dimensions(shape)), room)
197      +at = Lifecycle.natural_equal(U32.to_nat(index), previous, same)
198      Equal.trans(F32, Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index),
199        written, target,
200        Equal.trans(F32, Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index),
201          StorageLaws.latest(U32.to_nat(Shape.count(shape)), StorageLaws.Write{U32.from_nat(previous), written}, index, old), written,
202          step, write_hit(shape, previous, index, written, old, inside, at)),
203        hit(at))
204    case Shape.BFalse{other}:
205      +old = Replayed.value(shape, 0.0, history, index)
206      +step = Replayed.expected_snoc(history, StorageLaws.Write{U32.from_nat(previous), written}, U32.to_nat(Shape.count(shape)), index, 0.0)
207      +inside = Conversion.le_successor_lt(previous, Shape.logical_numel(Shape.dimensions(shape)), room)
208      +earlier = lt_succ_ne(U32.to_nat(index), previous, below, other)
209      Equal.trans(F32, Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index),
210        old, target,
211        Equal.trans(F32, Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index),
212          StorageLaws.latest(U32.to_nat(Shape.count(shape)), StorageLaws.Write{U32.from_nat(previous), written}, index, old), old,
213          step, write_miss(shape, previous, index, written, old, inside, earlier)),
214        rec(earlier))