def parallel_replayed_planned

bendtorch-core@0.1.0.0 · src/tensor/contracts/matmul_proof.bend:338

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/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws
import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend as Par

338def parallel_replayed_planned(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +rows: U32, +inner: U32, +right_inner: U32, +columns: U32,
339  -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>},
340  -re: {Shape.dimensions(right) == [right_inner, columns] : List<&2, U32>},
341  -oe: {Shape.dimensions(output) == [rows, columns] : List<&2, U32>},
342  -compatible: {U32.to_nat(inner) == U32.to_nat(right_inner) : Nat},
343  +planned: {Matrix.plan(left, right) == Done{Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible}} :
344    Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
345  +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
346  -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat},
347  +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>,
348  -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat},
349  -P: Result<&2, &1, Matrix.Error, Core.Dynamic & Core.Dynamic & Core.Dynamic> -> Type,
350  h: Laws.MatmulWith(left, right, Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible},
351    left_fill, left_ops, right_fill, right_ops, P)) ->
352  P(Matrix.matmul(Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}}, Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})):
353  +plan : Matrix.Plan<left, right> = Matrix.Plan{output, rows, inner, right_inner, columns, le, re, oe, compatible}
354  +facts : MatrixFacts<left, right, output, rows, inner, right_inner, columns> = plan_facts(left, right, plan, planned)
355  +oe_live = output_dimensions(left, right, output, rows, inner, right_inner, columns, facts)
356  parallel_lift(left, right, output, rows, inner, right_inner, columns, le, re, oe, compatible, planned,
357    left_fill, left_ops, left_fits, right_fill, right_ops, right_fits, P,
358    left_kept => left_values => left_words => a => right_kept => right_values => right_words => b => o =>
359      h(left_kept, left_words, a, right_kept, right_words, b, Par.writes(U32.to_nat(inner), U32.to_nat(columns), left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(Shape.count(output))),
360        row => row_below => column => column_below =>
361          parallel_cell(left, left_fill, left_ops, right, right_fill, right_ops, output, rows, inner, columns, oe_live,
362            row, row_below, column, column_below),
363        o))