src/tensor/contracts/sum_proof.bend
bendtorch-core@0.1.0.0 · 78 lines · 5 definitions
1import Base
2import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
3import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
4import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
5import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
6import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
7import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
8import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
9import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
10import bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend as Fold
11import bendtorch-core@0.1.0.0/src/tensor/contracts/fold_records.bend as Records
12import bendtorch-core@0.1.0.0/src/tensor/contracts/fold_proof.bend as Proof
13import bendtorch-core@0.1.0.0/src/tensor/contracts/sum.bend as Sum
14import bendtorch-core@0.1.0.0/src/tensor/contracts/LAWS.bend as Laws
15
16def sequential_snoc(+values: List<&2, F32>, +word: F32, +accumulator: F32) ->
17 {Reduction.sequential_sum(List.append(&2, F32, values, [word]), accumulator) ==
18 F32.add(Reduction.sequential_sum(values, accumulator), word) : F32}:
19 match values:
20 case Nil{}:
21 {==}
22 case +value <> +rest:
23 sequential_snoc(rest, word, F32.add(accumulator, value))
24
25def total_words(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat) ->
26 {Fold.total(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, count) ==
27 Reduction.sequential_sum(Laws.words(shape, fill, ops, count), 0.0) : F32}:
28 match count:
29 case 0n:
30 {==}
31 case 1n+previous:
32 +word = Replayed.value(shape, fill, ops, U32.from_nat(previous))
33 %Equal.sym(F32, Reduction.sequential_sum(List.append(&2, F32, Laws.words(shape, fill, ops, previous), [word]), 0.0),
34 F32.add(Reduction.sequential_sum(Laws.words(shape, fill, ops, previous), 0.0), word),
35 sequential_snoc(Laws.words(shape, fill, ops, previous), word, 0.0)) :
36 {F32.add(Fold.total(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, previous), word) == _ : F32}
37 Equal.cong(F32, F32, total => F32.add(total, word),
38 Fold.total(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, previous),
39 Reduction.sequential_sum(Laws.words(shape, fill, ops, previous), 0.0),
40 total_words(shape, fill, ops, previous))
41
42def position_inside(+count: Nat, +bound: Nat, +room: {Nat.is_le(count, bound) == True{} : Bool}) ->
43 {Pointwise.inside(~Unit, ~Sum.position, Unit{}, count, bound) == True{} : Bool}:
44 match count:
45 case 0n:
46 {==}
47 case 1n+previous:
48 %Equal.sym(Bool, Pointwise.inside(~Unit, ~Sum.position, Unit{}, previous, bound), True{},
49 position_inside(previous, bound, Conversion.le_predecessor(previous, bound, room))) :
50 {Bool.and(_, Nat.is_lt(previous, bound)) == True{} : Bool}
51 %Equal.sym(Bool, Nat.is_lt(previous, bound), True{}, Conversion.le_successor_lt(previous, bound, room)) :
52 {Bool.and(True{}, _) == True{} : Bool}
53 {==}
54
55def elements_room(+shape: Shape.Shape) ->
56 {Nat.is_le(Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
57 %Equal.sym(Nat, Shape.elements(shape), Shape.numel(Shape.extents(shape)), Shape.elements_exact(shape)) :
58 {Nat.is_le(_, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
59 Conversion.le_reflexive(Shape.logical_numel(Shape.dimensions(shape)))
60
61def sum_ordered(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
62 -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
63 Records.FoldContract<shape, Reduction.sequential_sum(Laws.words(shape, fill, ops, Shape.logical_numel(Shape.dimensions(shape))), 0.0),
64 other => Replayed.value(shape, fill, ops, other),
65 Sum.sum(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})>:
66 +count = Shape.elements(shape)
67 %Shape.elements_exact(shape) :
68 Records.FoldContract<shape, Reduction.sequential_sum(Laws.words(shape, fill, ops, _), 0.0),
69 other => Replayed.value(shape, fill, ops, other),
70 Fold.run(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, count,
71 Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})>
72 %total_words(shape, fill, ops, count) :
73 Records.FoldContract<shape, _,
74 other => Replayed.value(shape, fill, ops, other),
75 Fold.run(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, count,
76 Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})>
77 Proof.contract(~Unit, ~Sum.add, ~Unit, ~Sum.position, ~Sum.every, Unit{}, Unit{}, shape, fill, ops, count,
78 position_inside(count, Shape.logical_numel(Shape.dimensions(shape)), elements_room(shape)), fits)