src/tensor/contracts/pointwise_proof.bend
bendtorch-core@0.1.0.0 · 516 lines · 35 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/arith.bend as Arith
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/read_contract.bend as Reads
10import bendtorch-core@0.1.0.0/src/tensor/from_values_contract.bend as FromValues
11import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
12import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
13import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_records.bend as Records
14
15def append_nil(+ops: List<&2, StorageLaws.Op>) -> {List.append(&2, StorageLaws.Op, ops, Nil{}) == ops : List<&2, StorageLaws.Op>}:
16 match ops:
17 case Nil{}:
18 {==}
19 case +op <> +rest:
20 Equal.cong(List<&2, StorageLaws.Op>, List<&2, StorageLaws.Op>, tail => op <> tail,
21 List.append(&2, StorageLaws.Op, rest, Nil{}), rest, append_nil(rest))
22
23def append_snoc(+ops: List<&2, StorageLaws.Op>, +more: List<&2, StorageLaws.Op>, +last: StorageLaws.Op) ->
24 {List.append(&2, StorageLaws.Op, ops, Replayed.snoc(more, last)) ==
25 Replayed.snoc(List.append(&2, StorageLaws.Op, ops, more), last) : List<&2, StorageLaws.Op>}:
26 match ops:
27 case Nil{}:
28 {==}
29 case +op <> +rest:
30 Equal.cong(List<&2, StorageLaws.Op>, List<&2, StorageLaws.Op>, tail => op <> tail,
31 List.append(&2, StorageLaws.Op, rest, Replayed.snoc(more, last)),
32 Replayed.snoc(List.append(&2, StorageLaws.Op, rest, more), last), append_snoc(rest, more, last))
33
34def expected_append(+ops: List<&2, StorageLaws.Op>, +more: List<&2, StorageLaws.Op>, +n: Nat, +index: U32, +word: F32) ->
35 {StorageLaws.expected(List.append(&2, StorageLaws.Op, ops, more), n, index, word) ==
36 StorageLaws.expected(more, n, index, StorageLaws.expected(ops, n, index, word)) : F32}:
37 match ops:
38 case Nil{}:
39 {==}
40 case +op <> +rest:
41 expected_append(rest, more, n, index, StorageLaws.latest(n, op, index, word))
42
43def expected_reads(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +count: Nat, +n: Nat, +index: U32, +word: F32) ->
44 {StorageLaws.expected(Pointwise.reads(~P, ~map, plan, count), n, index, word) == word : F32}:
45 match count:
46 case 0n:
47 {==}
48 case 1n+previous:
49 Equal.trans(F32,
50 StorageLaws.expected(Pointwise.reads(~P, ~map, plan, 1n+previous), n, index, word),
51 StorageLaws.expected(Pointwise.reads(~P, ~map, plan, previous), n, index, word), word,
52 Replayed.expected_snoc(Pointwise.reads(~P, ~map, plan, previous), StorageLaws.Read{U32.from_nat(map(plan, previous))}, n, index, word),
53 expected_reads(~P, ~map, plan, previous, n, index, word))
54
55def value_reads(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +count: Nat, +shape: Shape.Shape, +fill: F32,
56 +ops: List<&2, StorageLaws.Op>, +index: U32) ->
57 {Replayed.value(shape, fill, List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, count)), index) ==
58 Replayed.value(shape, fill, ops, index) : F32}:
59 Equal.trans(F32,
60 Replayed.value(shape, fill, List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, count)), index),
61 StorageLaws.expected(Pointwise.reads(~P, ~map, plan, count), U32.to_nat(Shape.count(shape)), index, Replayed.value(shape, fill, ops, index)),
62 Replayed.value(shape, fill, ops, index),
63 expected_append(ops, Pointwise.reads(~P, ~map, plan, count), U32.to_nat(Shape.count(shape)), index, fill),
64 expected_reads(~P, ~map, plan, count, U32.to_nat(Shape.count(shape)), index, Replayed.value(shape, fill, ops, index)))
65
66def lt_add(+cursor: Nat, +rest: Nat) -> {Nat.is_lt(cursor, Nat.add(cursor, 1n+rest)) == True{} : Bool}:
67 match cursor:
68 case 0n:
69 {==}
70 case 1n+previous:
71 lt_add(previous, rest)
72
73def cursor_below(+cursor: Nat, +rest: Nat, +end: Nat, steps: {Nat.add(cursor, 1n+rest) == end : Nat}) ->
74 {Nat.is_lt(cursor, end) == True{} : Bool}:
75 %steps : {Nat.is_lt(cursor, _) == True{} : Bool}
76 lt_add(cursor, rest)
77
78def steps_next(+cursor: Nat, +rest: Nat, +end: Nat, steps: {Nat.add(cursor, 1n+rest) == end : Nat}) ->
79 {Nat.add(1n+cursor, rest) == end : Nat}:
80 Equal.trans(Nat, 1n+Nat.add(cursor, rest), Nat.add(cursor, 1n+rest), end,
81 Equal.sym(Nat, Nat.add(cursor, 1n+rest), 1n+Nat.add(cursor, rest), Arith.add_succ(cursor, rest)), steps)
82
83def steps_done(+cursor: Nat, +end: Nat, steps: {Nat.add(cursor, 0n) == end : Nat}) -> {cursor == end : Nat}:
84 Equal.trans(Nat, cursor, Nat.add(cursor, 0n), end, Equal.sym(Nat, Nat.add(cursor, 0n), cursor, Conversion.add_zero(cursor)), steps)
85
86def lt_succ_ne(+index: Nat, +previous: Nat, below: {Nat.is_lt(index, 1n+previous) == True{} : Bool},
87 other: {False{} == Nat.is_eq(index, previous) : Bool}) -> {Nat.is_lt(index, previous) == True{} : Bool}:
88 match index previous:
89 case 0n 0n:
90 Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, Arith.clash(other))
91 case 0n 1n+q:
92 {==}
93 case 1n+p 0n:
94 Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, Arith.lt_zero(p, below))
95 case 1n+p 1n+q:
96 lt_succ_ne(p, q, below, other)
97
98def lt_succ_le(+index: Nat, +bound: Nat, below: {Nat.is_lt(index, bound) == True{} : Bool}) ->
99 {Nat.is_le(1n+index, bound) == True{} : Bool}:
100 match index bound:
101 case 0n 0n:
102 Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, Arith.clash(below))
103 case 0n 1n+q:
104 Arith.le_zero(q)
105 case 1n+p 0n:
106 Empty.absurd({Nat.is_le(2n+p, 0n) == True{} : Bool}, Arith.clash(below))
107 case 1n+p 1n+q:
108 lt_succ_le(p, q, below)
109
110def inside_split(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +previous: Nat, +bound: Nat,
111 all: {Pointwise.inside(~P, ~map, plan, 1n+previous, bound) == True{} : Bool}, +index: Nat,
112 below: {Nat.is_lt(index, 1n+previous) == True{} : Bool},
113 rec: {Pointwise.inside(~P, ~map, plan, previous, bound) == True{} : Bool} -> {Nat.is_lt(index, previous) == True{} : Bool} ->
114 {Nat.is_lt(map(plan, index), bound) == True{} : Bool},
115 decision: Shape.BoolCase<Nat.is_eq(index, previous)>) -> {Nat.is_lt(map(plan, index), bound) == True{} : Bool}:
116 match decision:
117 case Shape.BTrue{same}:
118 %Equal.sym(Nat, index, previous, Lifecycle.natural_equal(index, previous, same)) : {Nat.is_lt(map(plan, _), bound) == True{} : Bool}
119 Arith.and_right(Pointwise.inside(~P, ~map, plan, previous, bound), Nat.is_lt(map(plan, previous), bound), all)
120 case Shape.BFalse{other}:
121 rec(Arith.and_left(Pointwise.inside(~P, ~map, plan, previous, bound), Nat.is_lt(map(plan, previous), bound), all),
122 lt_succ_ne(index, previous, below, other))
123
124def inside_at(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +count: Nat, +bound: Nat,
125 all: {Pointwise.inside(~P, ~map, plan, count, bound) == True{} : Bool}, +index: Nat,
126 below: {Nat.is_lt(index, count) == True{} : Bool}) -> {Nat.is_lt(map(plan, index), bound) == True{} : Bool}:
127 match count:
128 case 0n:
129 Empty.absurd({Nat.is_lt(map(plan, index), bound) == True{} : Bool}, Arith.lt_zero(index, below))
130 case 1n+previous:
131 inside_split(~P, ~map, plan, previous, bound, all, index, below,
132 earlier => before => inside_at(~P, ~map, plan, previous, bound, earlier, index, before),
133 Shape.bool_case(Nat.is_eq(index, previous)))
134
135def word_exact(+number: Nat, +shape: Shape.Shape,
136 below: {Nat.is_lt(number, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
137 {U32.to_nat(U32.from_nat(number)) == number : Nat}:
138 Conversion.natural_word_exact(number, Shape.count(shape),
139 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), Reads.count_exact(shape)) :
140 {Nat.is_le(number, _) == True{} : Bool}
141 Conversion.lt_le(number, Shape.logical_numel(Shape.dimensions(shape)), below))
142
143def word_inside(+number: Nat, +shape: Shape.Shape,
144 +below: {Nat.is_lt(number, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
145 {Nat.is_lt(U32.to_nat(U32.from_nat(number)), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}:
146 %Equal.sym(Nat, U32.to_nat(U32.from_nat(number)), number, word_exact(number, shape, below)) :
147 {Nat.is_lt(_, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
148 below
149
150def lt_count(+number: Nat, +shape: Shape.Shape,
151 below: {Nat.is_lt(number, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
152 {Nat.is_lt(number, U32.to_nat(Shape.count(shape))) == True{} : Bool}:
153 %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), Reads.count_exact(shape)) :
154 {Nat.is_lt(number, _) == True{} : Bool}
155 below
156
157def write_hit(+shape: Shape.Shape, +previous: Nat, +index: U32, +word: F32, +old: F32,
158 +room: {Nat.is_lt(previous, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
159 at: {U32.to_nat(index) == previous : Nat}) ->
160 {StorageLaws.latest(U32.to_nat(Shape.count(shape)), StorageLaws.Write{U32.from_nat(previous), word}, index, old) == word : F32}:
161 %Equal.sym(Nat, U32.to_nat(U32.from_nat(previous)), previous, word_exact(previous, shape, room)) :
162 {Bool.pick(F32, Bool.and(Nat.is_lt(_, U32.to_nat(Shape.count(shape))), Nat.is_eq(_, U32.to_nat(index))), word, old) == word : F32}
163 %Equal.sym(Nat, U32.to_nat(index), previous, at) :
164 {Bool.pick(F32, Bool.and(Nat.is_lt(previous, U32.to_nat(Shape.count(shape))), Nat.is_eq(previous, _)), word, old) == word : F32}
165 %Equal.sym(Bool, Nat.is_lt(previous, U32.to_nat(Shape.count(shape))), True{}, lt_count(previous, shape, room)) :
166 {Bool.pick(F32, Bool.and(_, Nat.is_eq(previous, previous)), word, old) == word : F32}
167 %Equal.sym(Bool, Nat.is_eq(previous, previous), True{}, Arith.eq_refl(previous)) :
168 {Bool.pick(F32, _, word, old) == word : F32}
169 {==}
170
171def write_miss(+shape: Shape.Shape, +previous: Nat, +index: U32, +word: F32, +old: F32,
172 +room: {Nat.is_lt(previous, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
173 earlier: {Nat.is_lt(U32.to_nat(index), previous) == True{} : Bool}) ->
174 {StorageLaws.latest(U32.to_nat(Shape.count(shape)), StorageLaws.Write{U32.from_nat(previous), word}, index, old) == old : F32}:
175 %Equal.sym(Nat, U32.to_nat(U32.from_nat(previous)), previous, word_exact(previous, shape, room)) :
176 {Bool.pick(F32, Bool.and(Nat.is_lt(_, U32.to_nat(Shape.count(shape))), Nat.is_eq(_, U32.to_nat(index))), word, old) == old : F32}
177 %Equal.sym(Bool, Nat.is_lt(previous, U32.to_nat(Shape.count(shape))), True{}, lt_count(previous, shape, room)) :
178 {Bool.pick(F32, Bool.and(_, Nat.is_eq(previous, U32.to_nat(index))), word, old) == old : F32}
179 %Equal.sym(Bool, Nat.is_eq(previous, U32.to_nat(index)), False{}, FromValues.lt_different(U32.to_nat(index), previous, earlier)) :
180 {Bool.pick(F32, _, word, old) == old : F32}
181 {==}
182
183
184
185def write_split(+shape: Shape.Shape, +history: List<&2, StorageLaws.Op>, +previous: Nat, +written: F32, +index: U32, +target: F32,
186 below: {Nat.is_lt(U32.to_nat(index), 1n+previous) == True{} : Bool},
187 +room: {Nat.is_le(1n+previous, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
188 hit: @at: {U32.to_nat(index) == previous : Nat} -> {written == target : F32},
189 rec: @earlier: {Nat.is_lt(U32.to_nat(index), previous) == True{} : Bool} -> {Replayed.value(shape, 0.0, history, index) == target : F32},
190 decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), previous)>) ->
191 {Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index) == target : F32}:
192 match decision:
193 case Shape.BTrue{same}:
194 +old = Replayed.value(shape, 0.0, history, index)
195 +step = Replayed.expected_snoc(history, StorageLaws.Write{U32.from_nat(previous), written}, U32.to_nat(Shape.count(shape)), index, 0.0)
196 +inside = Conversion.le_successor_lt(previous, Shape.logical_numel(Shape.dimensions(shape)), room)
197 +at = Lifecycle.natural_equal(U32.to_nat(index), previous, same)
198 Equal.trans(F32, Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index),
199 written, target,
200 Equal.trans(F32, Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index),
201 StorageLaws.latest(U32.to_nat(Shape.count(shape)), StorageLaws.Write{U32.from_nat(previous), written}, index, old), written,
202 step, write_hit(shape, previous, index, written, old, inside, at)),
203 hit(at))
204 case Shape.BFalse{other}:
205 +old = Replayed.value(shape, 0.0, history, index)
206 +step = Replayed.expected_snoc(history, StorageLaws.Write{U32.from_nat(previous), written}, U32.to_nat(Shape.count(shape)), index, 0.0)
207 +inside = Conversion.le_successor_lt(previous, Shape.logical_numel(Shape.dimensions(shape)), room)
208 +earlier = lt_succ_ne(U32.to_nat(index), previous, below, other)
209 Equal.trans(F32, Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index),
210 old, target,
211 Equal.trans(F32, Replayed.value(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(previous), written}), index),
212 StorageLaws.latest(U32.to_nat(Shape.count(shape)), StorageLaws.Write{U32.from_nat(previous), written}, index, old), old,
213 step, write_miss(shape, previous, index, written, old, inside, earlier)),
214 rec(earlier))
215
216def writes_value(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
217 +count: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
218 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape, +index: U32,
219 below: {Nat.is_lt(U32.to_nat(index), count) == True{} : Bool},
220 +room: {Nat.is_le(count, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
221 {Replayed.value(shape, 0.0, Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, count, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops), index) ==
222 Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)) : F32}:
223 match count:
224 case 0n:
225 Empty.absurd({Replayed.value(shape, 0.0, Nil{}, index) ==
226 Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)) : F32},
227 Arith.lt_zero(U32.to_nat(index), below))
228 case 1n+previous:
229 write_split(shape, Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, previous, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops),
230 previous, Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, previous), index,
231 Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)),
232 below, room,
233 at => Equal.cong(Nat, F32, position => Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, position),
234 previous, U32.to_nat(index), Equal.sym(Nat, U32.to_nat(index), previous, at)),
235 earlier => writes_value(~O, ~f, ~P, ~ia, ~ib, previous, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops,
236 shape, index, earlier, Conversion.le_predecessor(previous, Shape.logical_numel(Shape.dimensions(shape)), room)),
237 Shape.bool_case(Nat.is_eq(U32.to_nat(index), previous)))
238
239def input_storage(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +shape: Shape.Shape, +fill: F32,
240 +ops: List<&2, StorageLaws.Op>, +count: Nat) -> Storage.Storage:
241 Replayed.storage(shape, fill, List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, count)))
242
243def output_storage(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
244 +count: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
245 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape) -> Storage.Storage:
246 Replayed.storage(shape, 0.0, Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, count, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops))
247
248def Shaped(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
249 +fuel: Nat, +operation: O, +plan: P, +left: Shape.Shape, +right: Shape.Shape, +shape: Shape.Shape, +cursor: Nat,
250 -left_storage: Storage.Storage, -right_storage: Storage.Storage, -output_storage: Storage.Storage,
251 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type) -> Type:
252 @-left_fits: {Lifecycle.logical_length(left_storage) == Shape.logical_numel(Shape.dimensions(left)) : Nat} ->
253 @-right_fits: {Lifecycle.logical_length(right_storage) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
254 @-output_fits: {Lifecycle.logical_length(output_storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
255 Q(Pointwise.loop(~O, ~f, ~P, ~ia, ~ib, fuel, operation, plan, shape, cursor,
256 Pointwise.State{Core.Packed{left, Core.TTensor{left_storage, left_fits}}, Core.Packed{right, Core.TTensor{right_storage, right_fits}},
257 Core.TTensor{output_storage, output_fits}}))
258
259def Start(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
260 +fuel: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
261 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape, +cursor: Nat,
262 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type) -> Type:
263 Shaped(~O, ~f, ~P, ~ia, ~ib, fuel, operation, plan, left, right, shape, cursor,
264 input_storage(~P, ~ia, plan, left, left_fill, left_ops, cursor), input_storage(~P, ~ib, plan, right, right_fill, right_ops, cursor),
265 output_storage(~O, ~f, ~P, ~ia, ~ib, cursor, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape), Q)
266
267def Final(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
268 +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
269 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape, +count: Nat,
270 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type) -> Type:
271 @-left_fits: {Lifecycle.logical_length(input_storage(~P, ~ia, plan, left, left_fill, left_ops, count)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} ->
272 @-right_fits: {Lifecycle.logical_length(input_storage(~P, ~ib, plan, right, right_fill, right_ops, count)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
273 @-output_fits: {Lifecycle.logical_length(output_storage(~O, ~f, ~P, ~ia, ~ib, count, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape)) ==
274 Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
275 Q(((Core.Packed{left, Core.TTensor{input_storage(~P, ~ia, plan, left, left_fill, left_ops, count), left_fits}},
276 Core.Packed{right, Core.TTensor{input_storage(~P, ~ib, plan, right, right_fill, right_ops, count), right_fits}}),
277 Done{Core.Packed{shape, Core.TTensor{output_storage(~O, ~f, ~P, ~ia, ~ib, count, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape), output_fits}}}))
278
279def final_at(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
280 +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
281 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape, -end: Nat, -count: Nat,
282 same: {end == count : Nat},
283 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
284 h: Final(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, end, Q)) ->
285 Final(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, count, Q):
286 %same : Final(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, _, Q)
287 h
288
289def shift(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
290 +rest: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
291 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape, +cursor: Nat,
292 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
293 next: Start(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, 1n+cursor, Q)) ->
294 Shaped(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, left, right, shape, 1n+cursor,
295 Replayed.storage(left, left_fill, Replayed.snoc(List.append(&2, StorageLaws.Op, left_ops, Pointwise.reads(~P, ~ia, plan, cursor)),
296 StorageLaws.Read{U32.from_nat(ia(plan, cursor))})),
297 Replayed.storage(right, right_fill, Replayed.snoc(List.append(&2, StorageLaws.Op, right_ops, Pointwise.reads(~P, ~ib, plan, cursor)),
298 StorageLaws.Read{U32.from_nat(ib(plan, cursor))})),
299 Replayed.storage(shape, 0.0, Replayed.snoc(
300 Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, cursor, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops),
301 StorageLaws.Write{U32.from_nat(cursor),
302 f(operation, Replayed.value(left, left_fill, List.append(&2, StorageLaws.Op, left_ops, Pointwise.reads(~P, ~ia, plan, cursor)), U32.from_nat(ia(plan, cursor))),
303 Replayed.value(right, right_fill, List.append(&2, StorageLaws.Op, right_ops, Pointwise.reads(~P, ~ib, plan, cursor)), U32.from_nat(ib(plan, cursor))))})),
304 Q):
305 +left_read = {StorageLaws.Read{U32.from_nat(ia(plan, cursor))} : StorageLaws.Op}
306 +right_read = {StorageLaws.Read{U32.from_nat(ib(plan, cursor))} : StorageLaws.Op}
307 +left_seen = List.append(&2, StorageLaws.Op, left_ops, Pointwise.reads(~P, ~ia, plan, cursor))
308 +right_seen = List.append(&2, StorageLaws.Op, right_ops, Pointwise.reads(~P, ~ib, plan, cursor))
309 +x = Replayed.value(left, left_fill, left_seen, U32.from_nat(ia(plan, cursor)))
310 +y = Replayed.value(right, right_fill, right_seen, U32.from_nat(ib(plan, cursor)))
311 +left_word = Replayed.value(left, left_fill, left_ops, U32.from_nat(ia(plan, cursor)))
312 +right_word = Replayed.value(right, right_fill, right_ops, U32.from_nat(ib(plan, cursor)))
313 +history = Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, cursor, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops)
314 -left_after = Replayed.storage(left, left_fill, Replayed.snoc(left_seen, left_read))
315 -right_after = Replayed.storage(right, right_fill, Replayed.snoc(right_seen, right_read))
316 -output_after = Replayed.storage(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(cursor), f(operation, x, y)}))
317 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, ops => Replayed.storage(left, left_fill, ops),
318 List.append(&2, StorageLaws.Op, left_ops, Replayed.snoc(Pointwise.reads(~P, ~ia, plan, cursor), left_read)), Replayed.snoc(left_seen, left_read),
319 append_snoc(left_ops, Pointwise.reads(~P, ~ia, plan, cursor), left_read)) :
320 Shaped(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, left, right, shape, 1n+cursor, _, right_after, output_after, Q)
321 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, ops => Replayed.storage(right, right_fill, ops),
322 List.append(&2, StorageLaws.Op, right_ops, Replayed.snoc(Pointwise.reads(~P, ~ib, plan, cursor), right_read)), Replayed.snoc(right_seen, right_read),
323 append_snoc(right_ops, Pointwise.reads(~P, ~ib, plan, cursor), right_read)) :
324 Shaped(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, left, right, shape, 1n+cursor,
325 input_storage(~P, ~ia, plan, left, left_fill, left_ops, 1n+cursor), _, output_after, Q)
326 %Equal.cong(F32, Storage.Storage, word => Replayed.storage(shape, 0.0, Replayed.snoc(history, StorageLaws.Write{U32.from_nat(cursor), word})),
327 f(operation, left_word, right_word), f(operation, x, y),
328 Equal.trans(F32, f(operation, left_word, right_word), f(operation, x, right_word), f(operation, x, y),
329 Equal.cong(F32, F32, word => f(operation, word, right_word), left_word, x,
330 Equal.sym(F32, x, left_word, value_reads(~P, ~ia, plan, cursor, left, left_fill, left_ops, U32.from_nat(ia(plan, cursor))))),
331 Equal.cong(F32, F32, word => f(operation, x, word), right_word, y,
332 Equal.sym(F32, y, right_word, value_reads(~P, ~ib, plan, cursor, right, right_fill, right_ops, U32.from_nat(ib(plan, cursor))))))) :
333 Shaped(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, left, right, shape, 1n+cursor,
334 input_storage(~P, ~ia, plan, left, left_fill, left_ops, 1n+cursor), input_storage(~P, ~ib, plan, right, right_fill, right_ops, 1n+cursor), _, Q)
335 next
336
337def step_lift(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
338 +rest: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
339 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape, +cursor: Nat,
340 left_inside: {Nat.is_lt(U32.to_nat(U32.from_nat(ia(plan, cursor))), Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool},
341 right_inside: {Nat.is_lt(U32.to_nat(U32.from_nat(ib(plan, cursor))), Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool},
342 output_inside: {Nat.is_lt(U32.to_nat(U32.from_nat(cursor)), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
343 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
344 next: Start(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, 1n+cursor, Q)) ->
345 Start(~O, ~f, ~P, ~ia, ~ib, 1n+rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, cursor, Q):
346 +left_seen = List.append(&2, StorageLaws.Op, left_ops, Pointwise.reads(~P, ~ia, plan, cursor))
347 +right_seen = List.append(&2, StorageLaws.Op, right_ops, Pointwise.reads(~P, ~ib, plan, cursor))
348 +history = Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, cursor, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops)
349 +left_index = U32.from_nat(ia(plan, cursor))
350 +right_index = U32.from_nat(ib(plan, cursor))
351 +x = Replayed.value(left, left_fill, left_seen, left_index)
352 +y = Replayed.value(right, right_fill, right_seen, right_index)
353 left_fits => right_fits => output_fits =>
354 Replayed.read_lift(left, left_fill, left_seen, left_fits, left_index, left_inside,
355 pair => Q(Pointwise.left_step(~O, ~f, operation, shape, U32.from_nat(cursor), right_index,
356 state => Pointwise.loop(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, shape, 1n+cursor, state),
357 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_seen), right_fits}},
358 Core.TTensor{Replayed.storage(shape, 0.0, history), output_fits}, Core.read_dynamic_result(left, pair))),
359 left_after => Replayed.read_lift(right, right_fill, right_seen, right_fits, right_index, right_inside,
360 pair => Q(Pointwise.right_step(~O, ~f, operation, shape, U32.from_nat(cursor),
361 state => Pointwise.loop(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, shape, 1n+cursor, state),
362 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, Replayed.snoc(left_seen, StorageLaws.Read{left_index})), left_after}},
363 Core.TTensor{Replayed.storage(shape, 0.0, history), output_fits}, x, Core.read_dynamic_result(right, pair))),
364 right_after => Replayed.write_lift(shape, 0.0, history, output_fits, U32.from_nat(cursor), f(operation, x, y), output_inside,
365 pair => Q(Pointwise.write_step(shape,
366 state => Pointwise.loop(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, shape, 1n+cursor, state),
367 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, Replayed.snoc(left_seen, StorageLaws.Read{left_index})), left_after}},
368 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, Replayed.snoc(right_seen, StorageLaws.Read{right_index})), right_after}},
369 pair)),
370 output_after => shift(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, cursor,
371 Q, next)(left_after, right_after, output_after))))
372
373def loop_lift(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
374 +fuel: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
375 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape, +cursor: Nat,
376 +steps: {Nat.add(cursor, fuel) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
377 +left_inside: {Pointwise.inside(~P, ~ia, plan, Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool},
378 +right_inside: {Pointwise.inside(~P, ~ib, plan, Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool},
379 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
380 h: Final(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape,
381 Shape.logical_numel(Shape.dimensions(shape)), Q)) ->
382 Start(~O, ~f, ~P, ~ia, ~ib, fuel, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, cursor, Q):
383 match fuel:
384 case 0n:
385 final_at(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape,
386 Shape.logical_numel(Shape.dimensions(shape)), cursor,
387 Equal.sym(Nat, cursor, Shape.logical_numel(Shape.dimensions(shape)), steps_done(cursor, Shape.logical_numel(Shape.dimensions(shape)), steps)),
388 Q, h)
389 case 1n+rest:
390 +below = cursor_below(cursor, rest, Shape.logical_numel(Shape.dimensions(shape)), steps)
391 step_lift(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, cursor,
392 word_inside(ia(plan, cursor), left, inside_at(~P, ~ia, plan, Shape.logical_numel(Shape.dimensions(shape)),
393 Shape.logical_numel(Shape.dimensions(left)), left_inside, cursor, below)),
394 word_inside(ib(plan, cursor), right, inside_at(~P, ~ib, plan, Shape.logical_numel(Shape.dimensions(shape)),
395 Shape.logical_numel(Shape.dimensions(right)), right_inside, cursor, below)),
396 word_inside(cursor, shape, below), Q,
397 loop_lift(~O, ~f, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, 1n+cursor,
398 steps_next(cursor, rest, Shape.logical_numel(Shape.dimensions(shape)), steps), left_inside, right_inside, Q, h))
399
400def start_cast(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
401 +fuel: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
402 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape,
403 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
404 start: Start(~O, ~f, ~P, ~ia, ~ib, fuel, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, 0n, Q)) ->
405 Shaped(~O, ~f, ~P, ~ia, ~ib, fuel, operation, plan, left, right, shape, 0n,
406 Replayed.storage(left, left_fill, left_ops), Replayed.storage(right, right_fill, right_ops), Replayed.storage(shape, 0.0, Nil{}), Q):
407 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, ops => Replayed.storage(left, left_fill, ops),
408 List.append(&2, StorageLaws.Op, left_ops, Nil{}), left_ops, append_nil(left_ops)) :
409 Shaped(~O, ~f, ~P, ~ia, ~ib, fuel, operation, plan, left, right, shape, 0n,
410 _, Replayed.storage(right, right_fill, right_ops), Replayed.storage(shape, 0.0, Nil{}), Q)
411 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, ops => Replayed.storage(right, right_fill, ops),
412 List.append(&2, StorageLaws.Op, right_ops, Nil{}), right_ops, append_nil(right_ops)) :
413 Shaped(~O, ~f, ~P, ~ia, ~ib, fuel, operation, plan, left, right, shape, 0n,
414 input_storage(~P, ~ia, plan, left, left_fill, left_ops, 0n), _, Replayed.storage(shape, 0.0, Nil{}), Q)
415 start
416
417def run_lift(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
418 +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
419 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape,
420 +left_inside: {Pointwise.inside(~P, ~ia, plan, Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool},
421 +right_inside: {Pointwise.inside(~P, ~ib, plan, Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool},
422 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic> -> Type,
423 h: Final(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape,
424 Shape.logical_numel(Shape.dimensions(shape)), Q)) ->
425 @-left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat} ->
426 @-right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
427 Q(Pointwise.run(~O, ~f, ~P, ~ia, ~ib, operation, plan, shape,
428 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
429 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})):
430 left_fits => right_fits =>
431 Replayed.new_lift(shape, 0.0,
432 result => Q(Pointwise.allocated(~O, ~f, ~P, ~ia, ~ib, operation, plan, shape,
433 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
434 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}}, result)),
435 output_fits => start_cast(~O, ~f, ~P, ~ia, ~ib, Shape.elements(shape), operation, plan, left, left_fill, left_ops,
436 right, right_fill, right_ops, shape, Q,
437 loop_lift(~O, ~f, ~P, ~ia, ~ib, Shape.elements(shape), operation, plan, left, left_fill, left_ops, right, right_fill, right_ops,
438 shape, 0n, Shape.elements_exact(shape), left_inside, right_inside, Q, h))(left_fits, right_fits, output_fits))
439
440def dynamic_value(+shape: Shape.Shape, pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>) ->
441 {Core.dynamic_read_value(Core.read_dynamic_result(shape, pair)) == Core.read_value(shape, pair) : Maybe<&2, F32>}:
442 (tensor, result) = pair
443 {==}
444
445def replayed_point(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
446 -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, +index: U32,
447 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
448 {Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, index)) ==
449 Some{Replayed.value(shape, fill, ops, index)} : Maybe<&2, F32>}:
450 Equal.trans(Maybe<&2, F32>,
451 Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}}, index)),
452 Core.read_value(shape, Core.read_flat(shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}, index)),
453 Some{Replayed.value(shape, fill, ops, index)},
454 dynamic_value(shape, Core.read_flat(shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}, index)),
455 Replayed.read_found(shape, fill, ops, fits, index, inside))
456
457def input_point(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +count: Nat, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
458 -fits: {Lifecycle.logical_length(input_storage(~P, ~map, plan, shape, fill, ops, count)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
459 +index: U32, inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}) ->
460 {Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{input_storage(~P, ~map, plan, shape, fill, ops, count), fits}}, index)) ==
461 Some{Replayed.value(shape, fill, ops, index)} : Maybe<&2, F32>}:
462 +seen = List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~map, plan, count))
463 Equal.trans(Maybe<&2, F32>,
464 Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, seen), fits}}, index)),
465 Some{Replayed.value(shape, fill, seen, index)}, Some{Replayed.value(shape, fill, ops, index)},
466 replayed_point(shape, fill, seen, fits, index, inside),
467 Equal.cong(F32, Maybe<&2, F32>, word => Some{word}, Replayed.value(shape, fill, seen, index), Replayed.value(shape, fill, ops, index),
468 value_reads(~P, ~map, plan, count, shape, fill, ops, index)))
469
470def contract(~O: Data, ~f: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
471 +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
472 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +shape: Shape.Shape,
473 +left_inside: {Pointwise.inside(~P, ~ia, plan, Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool},
474 +right_inside: {Pointwise.inside(~P, ~ib, plan, Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool},
475 -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat},
476 -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}) ->
477 Records.PointwiseContract<shape, left, right,
478 index => Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, index),
479 other => Replayed.value(left, left_fill, left_ops, other), other => Replayed.value(right, right_fill, right_ops, other),
480 Pointwise.run(~O, ~f, ~P, ~ia, ~ib, operation, plan, shape,
481 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
482 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>:
483 +total = Shape.logical_numel(Shape.dimensions(shape))
484 Records.PointwiseContract{
485 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
486 result => {Pointwise.succeeded(result) == True{} : Bool},
487 left_after => right_after => output_after => {==})(left_fits, right_fits),
488 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
489 result => {Pointwise.output_dimensions(result) == Some{Shape.dimensions(shape)} : Maybe<&2, List<&2, U32>>},
490 left_after => right_after => output_after => {==})(left_fits, right_fits),
491 index => inside =>
492 +inside = inside
493 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
494 result => {Pointwise.output_point(result, index) ==
495 Some{Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index))} : Maybe<&2, F32>},
496 left_after => right_after => output_after =>
497 +history = Pointwise.writes(~O, ~f, ~P, ~ia, ~ib, total, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops)
498 Equal.trans(Maybe<&2, F32>,
499 Core.dynamic_read_value(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Replayed.storage(shape, 0.0, history), output_after}}, index)),
500 Some{Replayed.value(shape, 0.0, history, index)},
501 Some{Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index))},
502 replayed_point(shape, 0.0, history, output_after, index, inside),
503 Equal.cong(F32, Maybe<&2, F32>, word => Some{word}, Replayed.value(shape, 0.0, history, index),
504 Pointwise.cell(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, U32.to_nat(index)),
505 writes_value(~O, ~f, ~P, ~ia, ~ib, total, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, index,
506 inside, Conversion.le_reflexive(total)))))(left_fits, right_fits),
507 other => inside =>
508 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
509 result => {Pointwise.left_point(result, other) == Some{Replayed.value(left, left_fill, left_ops, other)} : Maybe<&2, F32>},
510 left_after => right_after => output_after =>
511 input_point(~P, ~ia, plan, total, left, left_fill, left_ops, left_after, other, inside))(left_fits, right_fits),
512 other => inside =>
513 run_lift(~O, ~f, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, shape, left_inside, right_inside,
514 result => {Pointwise.right_point(result, other) == Some{Replayed.value(right, right_fill, right_ops, other)} : Maybe<&2, F32>},
515 left_after => right_after => output_after =>
516 input_point(~P, ~ib, plan, total, right, right_fill, right_ops, right_after, other, inside))(left_fits, right_fits)}