src/tensor/contracts/dot_proof.bend
bendtorch-core@0.1.0.0 · 154 lines · 8 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
4import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
5import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
6import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
7import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
8import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
9import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
10import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold
11import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
12import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
13import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
14import bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend as Fold
15import bendtorch-core@0.1.0.0/src/tensor/contracts/fold_records.bend as Records
16import bendtorch-core@0.1.0.0/src/tensor/contracts/fold_proof.bend as Proof
17import bendtorch-core@0.1.0.0/src/tensor/contracts/dot.bend as Dot
18import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws
19
20def dot_snoc(+values: List<&2, DotFold.Factors>, +left: F32, +right: F32, +accumulator: F32) ->
21 {DotFold.dot_fold(List.append(&2, DotFold.Factors, values, [DotFold.Factors{left, right}]), accumulator) ==
22 F32.add(DotFold.dot_fold(values, accumulator), F32.mul(left, right)) : F32}:
23 match values:
24 case Nil{}:
25 {==}
26 case DotFold.Factors{+a, +b} <> +rest:
27 dot_snoc(rest, left, right, F32.add(accumulator, F32.mul(a, b)))
28
29def total_factors(+row: Nat, +column: Nat, +inner: Nat, +columns: Nat,
30 +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
31 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat) ->
32 {Fold.pair_total(~Unit, ~Dot.multiply_add, ~Dot.Cell, ~Dot.left_index, ~Dot.right_index, Unit{}, Dot.Cell{row, column, inner, columns},
33 left, left_fill, left_ops, right, right_fill, right_ops, count) ==
34 DotFold.dot_fold(Laws.factors(row, column, inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, count), 0.0) : F32}:
35 match count:
36 case 0n:
37 {==}
38 case 1n+previous:
39 +x = Replayed.value(left, left_fill, left_ops, U32.from_nat(Nat.add(Nat.mul(row, inner), previous)))
40 +y = Replayed.value(right, right_fill, right_ops, U32.from_nat(Nat.add(Nat.mul(previous, columns), column)))
41 +before = Laws.factors(row, column, inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous)
42 %Equal.sym(F32, DotFold.dot_fold(List.append(&2, DotFold.Factors, before, [DotFold.Factors{x, y}]), 0.0),
43 F32.add(DotFold.dot_fold(before, 0.0), F32.mul(x, y)), dot_snoc(before, x, y, 0.0)) :
44 {F32.add(Fold.pair_total(~Unit, ~Dot.multiply_add, ~Dot.Cell, ~Dot.left_index, ~Dot.right_index, Unit{},
45 Dot.Cell{row, column, inner, columns}, left, left_fill, left_ops, right, right_fill, right_ops, previous), F32.mul(x, y)) == _ : F32}
46 Equal.cong(F32, F32, total => F32.add(total, F32.mul(x, y)),
47 Fold.pair_total(~Unit, ~Dot.multiply_add, ~Dot.Cell, ~Dot.left_index, ~Dot.right_index, Unit{},
48 Dot.Cell{row, column, inner, columns}, left, left_fill, left_ops, right, right_fill, right_ops, previous),
49 DotFold.dot_fold(before, 0.0),
50 total_factors(row, column, inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, previous))
51
52def lt_mul_add(+a: Nat, +m: Nat, +b: Nat, +n: Nat, a_below: {Nat.is_lt(a, m) == True{} : Bool},
53 b_below: {Nat.is_lt(b, n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.mul(a, n), b), Nat.mul(m, n)) == True{} : Bool}:
54 match a m:
55 case 0n 0n:
56 Empty.absurd({Nat.is_lt(b, 0n) == True{} : Bool}, Arith.clash(a_below))
57 case 0n 1n+q:
58 Arith.lt_le_trans(b, n, Nat.add(n, Nat.mul(q, n)), b_below, Api.le_add_right(n, Nat.mul(q, n)))
59 case 1n+p 0n:
60 Empty.absurd({Nat.is_lt(Nat.add(Nat.add(n, Nat.mul(p, n)), b), 0n) == True{} : Bool}, Arith.clash(a_below))
61 case 1n+p 1n+q:
62 %Index.add_assoc(n, Nat.mul(p, n), b) : {Nat.is_lt(_, Nat.add(n, Nat.mul(q, n))) == True{} : Bool}
63 Api.lt_add_left(n, Nat.add(Nat.mul(p, n), b), Nat.mul(q, n), lt_mul_add(p, q, b, n, a_below, b_below))
64
65def left_below(+rows: Nat, +inner: Nat, +columns: Nat, +row: Nat, +column: Nat,
66 row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +left: Shape.Shape,
67 left_extents: {Shape.extents(left) == [rows, inner] : List<&2, Nat>}, +k: Nat, below: {Nat.is_lt(k, inner) == True{} : Bool}) ->
68 {Nat.is_lt(Dot.left_index(Dot.Cell{row, column, inner, columns}, k), Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool}:
69 %Equal.sym(List<&2, Nat>, Shape.extents(left), [rows, inner], left_extents) :
70 {Nat.is_lt(Nat.add(Nat.mul(row, inner), k), Shape.numel(_)) == True{} : Bool}
71 %Equal.sym(Nat, Nat.mul(inner, 1n), inner, Nats.mul_one_right(inner)) :
72 {Nat.is_lt(Nat.add(Nat.mul(row, inner), k), Nat.mul(rows, _)) == True{} : Bool}
73 lt_mul_add(row, rows, k, inner, row_below, below)
74
75def right_below(+inner: Nat, +columns: Nat, +row: Nat, +column: Nat,
76 column_below: {Nat.is_lt(column, columns) == True{} : Bool}, +right: Shape.Shape,
77 right_extents: {Shape.extents(right) == [inner, columns] : List<&2, Nat>}, +k: Nat, below: {Nat.is_lt(k, inner) == True{} : Bool}) ->
78 {Nat.is_lt(Dot.right_index(Dot.Cell{row, column, inner, columns}, k), Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool}:
79 %Equal.sym(List<&2, Nat>, Shape.extents(right), [inner, columns], right_extents) :
80 {Nat.is_lt(Nat.add(Nat.mul(k, columns), column), Shape.numel(_)) == True{} : Bool}
81 %Equal.sym(Nat, Nat.mul(columns, 1n), columns, Nats.mul_one_right(columns)) :
82 {Nat.is_lt(Nat.add(Nat.mul(k, columns), column), Nat.mul(inner, _)) == True{} : Bool}
83 lt_mul_add(k, inner, column, columns, below, column_below)
84
85def left_inside(+rows: Nat, +inner: Nat, +columns: Nat, +row: Nat, +column: Nat,
86 +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +left: Shape.Shape,
87 +left_extents: {Shape.extents(left) == [rows, inner] : List<&2, Nat>}, +count: Nat,
88 +room: {Nat.is_le(count, inner) == True{} : Bool}) ->
89 {Pointwise.inside(~Dot.Cell, ~Dot.left_index, Dot.Cell{row, column, inner, columns}, count, Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool}:
90 match count:
91 case 0n:
92 {==}
93 case 1n+previous:
94 +cell : Dot.Cell = Dot.Cell{row, column, inner, columns}
95 +bound = Shape.logical_numel(Shape.dimensions(left))
96 %Equal.sym(Bool, Pointwise.inside(~Dot.Cell, ~Dot.left_index, cell, previous, bound), True{},
97 left_inside(rows, inner, columns, row, column, row_below, left, left_extents, previous,
98 Conversion.le_predecessor(previous, inner, room))) :
99 {Bool.and(_, Nat.is_lt(Dot.left_index(cell, previous), bound)) == True{} : Bool}
100 %Equal.sym(Bool, Nat.is_lt(Dot.left_index(cell, previous), bound), True{},
101 left_below(rows, inner, columns, row, column, row_below, left, left_extents, previous,
102 Conversion.le_successor_lt(previous, inner, room))) :
103 {Bool.and(True{}, _) == True{} : Bool}
104 {==}
105
106def right_inside(+inner: Nat, +columns: Nat, +row: Nat, +column: Nat,
107 +column_below: {Nat.is_lt(column, columns) == True{} : Bool}, +right: Shape.Shape,
108 +right_extents: {Shape.extents(right) == [inner, columns] : List<&2, Nat>}, +count: Nat,
109 +room: {Nat.is_le(count, inner) == True{} : Bool}) ->
110 {Pointwise.inside(~Dot.Cell, ~Dot.right_index, Dot.Cell{row, column, inner, columns}, count, Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool}:
111 match count:
112 case 0n:
113 {==}
114 case 1n+previous:
115 +cell : Dot.Cell = Dot.Cell{row, column, inner, columns}
116 +bound = Shape.logical_numel(Shape.dimensions(right))
117 %Equal.sym(Bool, Pointwise.inside(~Dot.Cell, ~Dot.right_index, cell, previous, bound), True{},
118 right_inside(inner, columns, row, column, column_below, right, right_extents, previous,
119 Conversion.le_predecessor(previous, inner, room))) :
120 {Bool.and(_, Nat.is_lt(Dot.right_index(cell, previous), bound)) == True{} : Bool}
121 %Equal.sym(Bool, Nat.is_lt(Dot.right_index(cell, previous), bound), True{},
122 right_below(inner, columns, row, column, column_below, right, right_extents, previous,
123 Conversion.le_successor_lt(previous, inner, room))) :
124 {Bool.and(True{}, _) == True{} : Bool}
125 {==}
126
127def dot_ordered(+rows: Nat, +inner: Nat, +columns: Nat, +row: Nat, +row_below: {Nat.is_lt(row, rows) == True{} : Bool},
128 +column: Nat, +column_below: {Nat.is_lt(column, columns) == True{} : Bool},
129 +left: Shape.Shape, +left_extents: {Shape.extents(left) == [rows, inner] : List<&2, Nat>},
130 +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
131 -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat},
132 +right: Shape.Shape, +right_extents: {Shape.extents(right) == [inner, columns] : List<&2, Nat>},
133 +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>,
134 -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}) ->
135 Records.PairFoldContract<left, right,
136 DotFold.dot_fold(Laws.factors(row, column, inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, inner), 0.0),
137 other => Replayed.value(left, left_fill, left_ops, other),
138 other => Replayed.value(right, right_fill, right_ops, other),
139 Dot.dot(Dot.Cell{row, column, inner, columns},
140 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
141 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>:
142 +cell : Dot.Cell = Dot.Cell{row, column, inner, columns}
143 %total_factors(row, column, inner, columns, left, left_fill, left_ops, right, right_fill, right_ops, inner) :
144 Records.PairFoldContract<left, right, _,
145 other => Replayed.value(left, left_fill, left_ops, other),
146 other => Replayed.value(right, right_fill, right_ops, other),
147 Fold.pair_run(~Unit, ~Dot.multiply_add, ~Dot.Cell, ~Dot.left_index, ~Dot.right_index, Unit{}, cell, inner,
148 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
149 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>
150 Proof.pair_contract(~Unit, ~Dot.multiply_add, ~Dot.Cell, ~Dot.left_index, ~Dot.right_index, Unit{}, cell,
151 left, left_fill, left_ops, right, right_fill, right_ops, inner,
152 left_inside(rows, inner, columns, row, column, row_below, left, left_extents, inner, Conversion.le_reflexive(inner)),
153 right_inside(inner, columns, row, column, column_below, right, right_extents, inner, Conversion.le_reflexive(inner)),
154 left_fits, right_fits)