src/tensor/contracts/PROOF.bend
bendtorch-core@0.1.0.0 · 52 lines · 0 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues
3import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws
4import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
5import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as Proof
6import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast_proof.bend as BroadcastProof
7import bendtorch-core@0.1.0.0/src/tensor/contracts/sum_proof.bend as SumProof
8import bendtorch-core@0.1.0.0/src/tensor/contracts/dot_proof.bend as DotProof
9import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_proof.bend as MatmulOrdered
10import bendtorch-core@0.1.0.0/src/tensor/contracts/product_proof.bend as ProductOrdered
11import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix
12
13def Laws.new_replayed(shape, fill, P, h):
14 Replayed.new_lift(shape, fill, P, h)
15
16def Laws.from_values_replayed(shape, values, counted, P, h):
17 +counted = counted
18 FromValues.from_values_lift(shape, values, counted, P, h)
19
20def Laws.replayed_read(shape, fill, ops, fits, index, inside):
21 Proof.replayed_point(shape, fill, ops, fits, index, inside)
22
23def Laws.broadcast_pointwise(operation, plan, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits):
24 BroadcastProof.broadcast_pointwise(operation, plan, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits)
25
26def Laws.sum_ordered(shape, fill, ops, fits):
27 SumProof.sum_ordered(shape, fill, ops, fits)
28
29def Laws.dot_ordered(rows, inner, columns, row, row_below, column, column_below, left, left_extents, left_fill, left_ops, left_fits,
30 right, right_extents, right_fill, right_ops, right_fits):
31 DotProof.dot_ordered(rows, inner, columns, row, row_below, column, column_below, left, left_extents, left_fill, left_ops, left_fits,
32 right, right_extents, right_fill, right_ops, right_fits)
33
34def Laws.matmul_ordered(left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits):
35 MatmulOrdered.matmul_ordered(left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits)
36
37def Laws.matmul_replayed(left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits, P, h):
38 MatmulOrdered.matmul_replayed(left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits, P, h)
39
40def Laws.product_ordered(lo, ro, left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits):
41 ProductOrdered.product_ordered(lo, ro, left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits)
42
43def Laws.product_replayed(lo, ro, left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits, P, h):
44 ProductOrdered.product_replayed(lo, ro, left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits, P, h)
45
46def Laws.matmul_nt_ordered(left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits):
47 ProductOrdered.product_ordered(Matrix.Kept{}, Matrix.Kept{}, left, right, plan, planned, left_fill, left_ops, left_fits,
48 right_fill, right_ops, right_fits)
49
50def Laws.matmul_tn_ordered(left, right, plan, planned, left_fill, left_ops, left_fits, right_fill, right_ops, right_fits):
51 ProductOrdered.product_ordered(Matrix.Swapped{}, Matrix.Swapped{}, left, right, plan, planned, left_fill, left_ops, left_fits,
52 right_fill, right_ops, right_fits)