def output_eq

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned
import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

752# The writes of every cell, replayed on the owned storage `created` makes for
753# the output, give the owned storage the parallel build fills.
754def output_eq(+span: Nat, +columns: Nat, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +ha: List<&2, Api.Effect>, +dl: Nat, +fa: F32, +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +hb: List<&2, Api.Effect>, +dr: Nat, +fb: F32, +lsrc: Source<left, left_fill, left_ops, ha, dl, fa>, +rsrc: Source<right, right_fill, right_ops, hb, dr, fb>,
755  +output: Shape.Shape, +rows: Nat,
756  +left_extents: {Shape.extents(left) == [rows, span] : List<&2, Nat>},
757  +right_extents: {Shape.extents(right) == [span, columns] : List<&2, Nat>},
758  +output_extents: {Shape.extents(output) == [rows, columns] : List<&2, Nat>},
759  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(output))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(output))) == True{} : Bool}) ->
760  {StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output))), Storage.Owned{d, U32.to_nat(Shape.count(output)), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, U32.to_nat(Shape.count(output)), Matrix.build(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), Matrix.build_balanced(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), f} : Storage.Storage}:
761  Equal.trans(Storage.Storage, StorageLaws.replay(writes(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output))), Storage.Owned{d, U32.to_nat(Shape.count(output)), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}),
762    Storage.Owned{d, U32.to_nat(Shape.count(output)), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n), out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n), f},
763    Storage.Owned{d, U32.to_nat(Shape.count(output)), Matrix.build(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), Matrix.build_balanced(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), f},
764    chain(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, d, U32.to_nat(Shape.count(output)), f, fits, Shape.count(output), Conversion.le_reflexive(U32.to_nat(Shape.count(output))), U32.to_nat(Shape.count(output)), Conversion.le_reflexive(U32.to_nat(Shape.count(output)))),
765    Owned.owned_eq(d, U32.to_nat(Shape.count(output)), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n), Matrix.build(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)),
766      Equal.sym(Array<F32>, Matrix.build(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb)), out_spec(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n),
767        build_eq(span, columns, left, left_fill, left_ops, ha, dl, fa, right, right_fill, right_ops, hb, dr, fb, U32.to_nat(Shape.count(output)), lsrc, rsrc, output, rows, left_extents, right_extents, output_extents, Reads.count_exact(output), d, Matrix.product_splits(d, span), 0n)),
768      out_balanced(span, columns, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output)), d, 0n), f)(Matrix.build_balanced(d, Matrix.product_splits(d, span), span, columns, U32.to_nat(Shape.count(output)), 0n, Api.arr(ha, dl, fa), Api.arr(hb, dr, fb))))