src/tensor/clone_contract.bend
bendtorch-core@0.1.0.0 · 186 lines · 20 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/main.bend as Storage
4import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
5import bendtorch-core@0.1.0.0/src/storage/PROOF.bend as StorageProof
6import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
7import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
8import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
9import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation
10import bendtorch-core@0.1.0.0/src/tensor/read_contract.bend as Reads
11import bendtorch-core@0.1.0.0/src/tensor/write_contract.bend as Writes
12import bendtorch-core@0.1.0.0/src/tensor/clone_metadata_records.bend as Laws
13
14def first_value_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32,
15 pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
16 {Observation.clone_first_value_pair(shape, other, Core.clone_result(shape, original, valid, pair, same)) ==
17 Lifecycle.read_value(Storage.get(StorageLaws.owner(Storage.Storage, pair), other)) : Maybe<&2, F32>}:
18 (first, second) = pair
19 Core.read_result_value(shape, first,
20 Equal.trans(Nat, Lifecycle.logical_length(first), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
21 %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
22 {Lifecycle.first_length(_) == Lifecycle.logical_length(original) : Nat}
23 Lifecycle.clone_first_length(original), valid),
24 other, Storage.get(first, other), {==})
25
26def untouched_value(-shape: Shape.Shape, +other: U32, written: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
27 storage: Storage.Storage, -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
28 {Observation.untouched(shape, other, written, Core.TTensor{storage, valid}) == Lifecycle.read_value(Storage.get(storage, other)) : Maybe<&2, F32>}:
29 (tensor, result) = written
30 Core.read_result_value(shape, storage, valid, other, Storage.get(storage, other), {==})
31
32def second_value_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32,
33 pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
34 {Observation.clone_second_value_pair(shape, other, Core.clone_result(shape, original, valid, pair, same)) ==
35 Lifecycle.read_value(Storage.get(StorageLaws.outcome(Storage.Storage, pair), other)) : Maybe<&2, F32>}:
36 (first, second) = pair
37 Core.read_result_value(shape, second,
38 Equal.trans(Nat, Lifecycle.logical_length(second), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
39 %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
40 {Lifecycle.second_length(_) == Lifecycle.logical_length(original) : Nat}
41 Lifecycle.clone_second_length(original), valid),
42 other, Storage.get(second, other), {==})
43
44def first_written_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, +other: U32,
45 pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
46 {Observation.clone_written_first_pair(shape, index, value, other, Core.clone_result(shape, original, valid, pair, same)) ==
47 Lifecycle.read_value(Storage.get(StorageLaws.written(StorageLaws.owner(Storage.Storage, pair), index, value), other)) : Maybe<&2, F32>}:
48 (first, second) = pair
49 Writes.write_value_projection(shape, first,
50 Equal.trans(Nat, Lifecycle.logical_length(first), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
51 %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
52 {Lifecycle.first_length(_) == Lifecycle.logical_length(original) : Nat}
53 Lifecycle.clone_first_length(original), valid),
54 index, value, other, Storage.set(first, index, value), {==})
55
56def second_written_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, +other: U32,
57 pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
58 {Observation.clone_written_second_pair(shape, index, value, other, Core.clone_result(shape, original, valid, pair, same)) ==
59 Lifecycle.read_value(Storage.get(StorageLaws.outcome(Storage.Storage, pair), other)) : Maybe<&2, F32>}:
60 (first, second) = pair
61 untouched_value(shape, other, Core.write_flat(shape, Core.TTensor{first, Equal.trans(Nat, Lifecycle.logical_length(first), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
62 %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
63 {Lifecycle.first_length(_) == Lifecycle.logical_length(original) : Nat}
64 Lifecycle.clone_first_length(original), valid)}, index, value), second,
65 Equal.trans(Nat, Lifecycle.logical_length(second), Lifecycle.logical_length(original), Shape.logical_numel(Shape.dimensions(shape)),
66 %Equal.sym(Storage.Storage & Storage.Storage, (first, second), Storage.clone(original), same) :
67 {Lifecycle.second_length(_) == Lifecycle.logical_length(original) : Nat}
68 Lifecycle.clone_second_length(original), valid))
69
70def first_length_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
71 {Observation.clone_first_length_pair(shape, Core.clone_result(shape, original, valid, pair, same)) == Lifecycle.first_length(pair) : Nat}:
72 (first, second) = pair
73 {==}
74
75def second_length_projection(-shape: Shape.Shape, -original: Storage.Storage, -valid: {Lifecycle.logical_length(original) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, pair: Storage.Storage & Storage.Storage, -same: {pair == Storage.clone(original) : Storage.Storage & Storage.Storage}) ->
76 {Observation.clone_second_length_pair(shape, Core.clone_result(shape, original, valid, pair, same)) == Lifecycle.second_length(pair) : Nat}:
77 (first, second) = pair
78 {==}
79
80def first_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>) ->
81 {Observation.clone_first_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
82 (first, second) = pair
83 {==}
84
85def second_dimensions_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>) ->
86 {Observation.clone_second_dimensions_pair(shape, pair) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>}:
87 (first, second) = pair
88 {==}
89
90def first_count_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>) ->
91 {Observation.clone_first_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
92 (first, second) = pair
93 {==}
94
95def second_count_pair(+shape: Shape.Shape, pair: Core.Tensor<shape> & Core.Tensor<shape>) ->
96 {Observation.clone_second_count_pair(shape, pair) == Some{Shape.count(shape)} : Maybe<&2, U32>}:
97 (first, second) = pair
98 {==}
99
100def first_value_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
101 {Observation.clone_first_value(shape, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
102 Equal.trans(Maybe<&2, F32>, Observation.clone_first_value_pair(shape, other, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})),
103 Lifecycle.read_value(Storage.get(StorageLaws.first(StorageLaws.created(Shape.count(shape), fill)), other)), Some{fill},
104 first_value_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, other, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
105 Reads.stored_value(StorageLaws.first(StorageLaws.created(Shape.count(shape), fill)), other, fill,
106 StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.First{}], other, Conversion.shape_count_within(shape), Reads.word_inside(shape, other, inside))))
107
108def second_value_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
109 {Observation.clone_second_value(shape, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
110 Equal.trans(Maybe<&2, F32>, Observation.clone_second_value_pair(shape, other, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})),
111 Lifecycle.read_value(Storage.get(StorageLaws.second(StorageLaws.created(Shape.count(shape), fill)), other)), Some{fill},
112 second_value_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, other, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
113 Reads.stored_value(StorageLaws.second(StorageLaws.created(Shape.count(shape), fill)), other, fill,
114 StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.Second{}], other, Conversion.shape_count_within(shape), Reads.word_inside(shape, other, inside))))
115
116def first_written_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
117 {Observation.clone_written_first(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Writes.written_pick(shape, index, value, other, fill)} : Maybe<&2, F32>}:
118 Equal.trans(Maybe<&2, F32>, Observation.clone_written_first_pair(shape, index, value, other, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})),
119 Lifecycle.read_value(Storage.get(StorageLaws.written(StorageLaws.first(StorageLaws.created(Shape.count(shape), fill)), index, value), other)),
120 Some{Writes.written_pick(shape, index, value, other, fill)},
121 first_written_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, other, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
122 Reads.stored_value(StorageLaws.written(StorageLaws.first(StorageLaws.created(Shape.count(shape), fill)), index, value), other, Writes.written_pick(shape, index, value, other, fill),
123 StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.First{}, StorageLaws.Write{index, value}], other, Conversion.shape_count_within(shape),
124 Reads.word_inside(shape, other, inside))))
125
126def second_written_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32, +value: F32, +other: U32, inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
127 {Observation.clone_written_second(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{fill} : Maybe<&2, F32>}:
128 Equal.trans(Maybe<&2, F32>, Observation.clone_written_second_pair(shape, index, value, other, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})),
129 Lifecycle.read_value(Storage.get(StorageLaws.second(StorageLaws.created(Shape.count(shape), fill)), other)), Some{fill},
130 second_written_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, index, value, other, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
131 Reads.stored_value(StorageLaws.second(StorageLaws.created(Shape.count(shape), fill)), other, fill,
132 StorageLaws.replay_get(Shape.count(shape), fill, [StorageLaws.Second{}], other, Conversion.shape_count_within(shape), Reads.word_inside(shape, other, inside))))
133
134def first_length_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
135 {Observation.clone_first_length(shape, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
136 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, Observation.clone_first_length_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Shape.logical_numel(Shape.dimensions(shape)),
137 Equal.trans(Nat, Observation.clone_first_length_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Lifecycle.first_length(Storage.clone(StorageLaws.created(Shape.count(shape), fill))), Shape.logical_numel(Shape.dimensions(shape)),
138 first_length_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
139 Equal.trans(Nat, Lifecycle.first_length(Storage.clone(StorageLaws.created(Shape.count(shape), fill))), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
140 Lifecycle.clone_first_length(StorageLaws.created(Shape.count(shape), fill)), Reads.created_exact(shape, fill))))
141
142def second_length_done(+shape: Shape.Shape, +fill: F32, -valid: {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
143 {Observation.clone_second_length(shape, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>}:
144 Equal.cong(Nat, Maybe<&2, Nat>, number => Some{number}, Observation.clone_second_length_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Shape.logical_numel(Shape.dimensions(shape)),
145 Equal.trans(Nat, Observation.clone_second_length_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid})), Lifecycle.second_length(Storage.clone(StorageLaws.created(Shape.count(shape), fill))), Shape.logical_numel(Shape.dimensions(shape)),
146 second_length_projection(shape, StorageLaws.created(Shape.count(shape), fill), valid, Storage.clone(StorageLaws.created(Shape.count(shape), fill)), {==}),
147 Equal.trans(Nat, Lifecycle.second_length(Storage.clone(StorageLaws.created(Shape.count(shape), fill))), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
148 Lifecycle.clone_second_length(StorageLaws.created(Shape.count(shape), fill)), Reads.created_exact(shape, fill))))
149
150def clone_written(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32, +other: U32, -expected: F32,
151 inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}, picked: {Writes.written_pick(shape, index, value, other, fill) == expected : F32}) ->
152 {Observation.clone_written_first(shape, index, value, other, Core.new(shape, fill)) == Some{expected} : Maybe<&2, F32>}:
153 Reads.new_lift(shape, fill, result => {Observation.clone_written_first(shape, index, value, other, result) == Some{expected} : Maybe<&2, F32>},
154 valid => Equal.trans(Maybe<&2, F32>, Observation.clone_written_first(shape, index, value, other, Done{Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}}),
155 Some{Writes.written_pick(shape, index, value, other, fill)}, Some{expected},
156 first_written_done(shape, fill, valid, index, value, other, inside),
157 Equal.cong(F32, Maybe<&2, F32>, number => Some{number}, Writes.written_pick(shape, index, value, other, fill), expected, picked)))
158
159def clone_contract(+shape: Shape.Shape, +fill: F32) -> Laws.CloneContract<shape, fill>:
160 Laws.CloneContract{
161 Reads.new_lift(shape, fill, result => {Observation.clone_first_dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
162 valid => first_dimensions_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
163 Reads.new_lift(shape, fill, result => {Observation.clone_second_dimensions(shape, result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
164 valid => second_dimensions_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
165 Reads.new_lift(shape, fill, result => {Observation.clone_first_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
166 valid => first_length_done(shape, fill, valid)),
167 Reads.new_lift(shape, fill, result => {Observation.clone_second_length(shape, result) == Some{Shape.logical_numel(Shape.dimensions(shape))} : Maybe<&2, Nat>},
168 valid => second_length_done(shape, fill, valid)),
169 Reads.new_lift(shape, fill, result => {Observation.clone_first_count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
170 valid => first_count_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
171 Reads.new_lift(shape, fill, result => {Observation.clone_second_count(shape, result) == Some{Shape.count(shape)} : Maybe<&2, U32>},
172 valid => second_count_pair(shape, Core.clone(shape, Core.TTensor{StorageLaws.created(Shape.count(shape), fill), valid}))),
173 other => inside => Reads.new_lift(shape, fill, result => {Observation.clone_first_value(shape, other, result) == Some{fill} : Maybe<&2, F32>},
174 valid => first_value_done(shape, fill, valid, other, inside)),
175 other => inside => Reads.new_lift(shape, fill, result => {Observation.clone_second_value(shape, other, result) == Some{fill} : Maybe<&2, F32>},
176 valid => second_value_done(shape, fill, valid, other, inside))}
177
178def clone_write(+shape: Shape.Shape, +fill: F32, +index: U32, +value: F32,
179 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) -> Laws.CloneWrite<shape, fill, index, value>:
180 +inside = inside
181 Laws.CloneWrite{
182 clone_written(shape, fill, index, value, index, value, inside, Writes.pick_hit(shape, index, value, fill, inside)),
183 other => inside_other => different =>
184 clone_written(shape, fill, index, value, other, fill, inside_other, Writes.pick_frame(shape, index, value, other, fill, inside, different)),
185 other => inside_other => Reads.new_lift(shape, fill, result => {Observation.clone_written_second(shape, index, value, other, result) == Some{fill} : Maybe<&2, F32>},
186 valid => second_written_done(shape, fill, valid, index, value, other, inside_other))}