MatmulParallelProof.source_read: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend as MatmulParallelProof
Lines 463-481 of bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&start_line=463&end_line=481

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

def source_read(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +d: Nat, +f: F32,
  +source: Source<shape, fill, ops, h, d, f>, +index: U32,
  +inside: {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(shape))) == True{} : Bool}, -pair: Array<F32> & F32,
  +exact: {pair == Array.get(F32, Api.arr(h, d, f), index) : Array<F32> & F32}) ->
  {Refinement.second(F32, pair) == Replayed.value(shape, fill, ops, index) : F32}:
  match source:
    case NoCells{zero}:
      Empty.absurd({Refinement.second(F32, pair) == Replayed.value(shape, fill, ops, index) : F32},
        Arith.lt_zero(U32.to_nat(index),
          %zero : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
          inside))
    case Normal{fits, same, filled}:
      Equal.trans(F32, Refinement.second(F32, pair), Api.current(h, index, f), Replayed.value(shape, fill, ops, index),
        Build.got_value(d, h, f, U32.to_nat(Shape.count(shape)), index, pair, exact, fits, inside,
          %Equal.sym(List<&2, Api.Effect>, h, history(shape, ops), same) : {Build.written(U32.to_nat(Shape.count(shape)), _) == True{} : Bool}
          copy_valid(shape, ops)),
        %Equal.sym(List<&2, Api.Effect>, h, history(shape, ops), same) : {Api.current(_, index, f) == Replayed.value(shape, fill, ops, index) : F32}
        %Equal.sym(F32, f, fill, filled) : {Api.current(history(shape, ops), index, _) == Replayed.value(shape, fill, ops, index) : F32}
        copy_word(shape, fill, ops, index))

Uses (28):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=count
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=Effect
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=current
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=lt_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=second
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend&name=got_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_build_proof.bend&name=written
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=Source
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=copy_valid
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=copy_word
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=history
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend&name=value