def source_read

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

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/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend as Build
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

463def source_read(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32,
464  +source: Source<shape, fill, ops, h, d, f>, +index: U32,
465  +inside: {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == True{} : Bool}, -pair: Array<F32> & F32,
466  +exact: {pair == Array.get(F32, Api.arr(h, d, f), index) : Array<F32> & F32}) ->
467  {Refinement.second(F32, pair) == Replayed.value(shape, fill, ops, index) : F32}:
468  match source:
469    case NoCells{zero}:
470      Empty.absurd({Refinement.second(F32, pair) == Replayed.value(shape, fill, ops, index) : F32},
471        Arith.lt_zero(U32.to_nat(index),
472          %zero : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
473          inside))
474    case Normal{fits, same, filled}:
475      Equal.trans(F32, Refinement.second(F32, pair), Api.current(h, index, f), Replayed.value(shape, fill, ops, index),
476        Build.got_value(d, h, f, U32.to_nat(Shape.count(shape)), index, pair, exact, fits, inside,
477          %Equal.sym(List<&2, Api.Effect>, h, history(shape, ops), same) : {Build.written(U32.to_nat(Shape.count(shape)), _) == True{} : Bool}
478          copy_valid(shape, ops)),
479        %Equal.sym(List<&2, Api.Effect>, h, history(shape, ops), same) : {Api.current(_, index, f) == Replayed.value(shape, fill, ops, index) : F32}
480        %Equal.sym(F32, f, fill, filled) : {Api.current(history(shape, ops), index, _) == Replayed.value(shape, fill, ops, index) : F32}
481        copy_word(shape, fill, ops, index))