src/tensor/contracts/fold_proof.bend
bendtorch-core@0.1.0.0 · 321 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/tensor/core.bend as Core
6import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
7import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
8import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
9import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
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
12
13def Shaped(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
14 +fuel: Nat, +operation: O, +plan: P, +shape: Shape.Shape, +cursor: Nat, -storage: Storage.Storage, +accumulator: F32,
15 -Q: Core.Dynamic & Result<&2, &1, Core.Error, F32> -> Type) -> Type:
16 @-fits: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
17 Q(Fold.loop(~O, ~g, ~P, ~ia, ~keep, fuel, operation, plan, cursor, Core.Packed{shape, Core.TTensor{storage, fits}}, accumulator))
18
19def Start(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
20 +fuel: Nat, +operation: O, +plan: P, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +cursor: Nat,
21 -Q: Core.Dynamic & Result<&2, &1, Core.Error, F32> -> Type) -> Type:
22 Shaped(~O, ~g, ~P, ~ia, ~keep, fuel, operation, plan, shape, cursor, PointwiseProof.input_storage(~P, ~ia, plan, shape, fill, ops, cursor),
23 Fold.total(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, cursor), Q)
24
25def Final(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
26 +operation: O, +plan: P, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat,
27 -Q: Core.Dynamic & Result<&2, &1, Core.Error, F32> -> Type) -> Type:
28 @-fits: {Lifecycle.logical_length(PointwiseProof.input_storage(~P, ~ia, plan, shape, fill, ops, count)) ==
29 Shape.logical_numel(Shape.dimensions(shape)) : Nat} ->
30 Q((Core.Packed{shape, Core.TTensor{PointwiseProof.input_storage(~P, ~ia, plan, shape, fill, ops, count), fits}},
31 Done{Fold.total(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, count)}))
32
33def final_at(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
34 +operation: O, +plan: P, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, -end: Nat, -count: Nat,
35 same: {end == count : Nat}, -Q: Core.Dynamic & Result<&2, &1, Core.Error, F32> -> Type,
36 h: Final(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, end, Q)) ->
37 Final(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, count, Q):
38 %same : Final(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, _, Q)
39 h
40
41def shift(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
42 +rest: Nat, +operation: O, +plan: P, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +cursor: Nat,
43 -Q: Core.Dynamic & Result<&2, &1, Core.Error, F32> -> Type,
44 next: Start(~O, ~g, ~P, ~ia, ~keep, rest, operation, plan, shape, fill, ops, 1n+cursor, Q)) ->
45 Shaped(~O, ~g, ~P, ~ia, ~keep, rest, operation, plan, shape, 1n+cursor,
46 Replayed.storage(shape, fill, Replayed.snoc(List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~ia, plan, cursor)),
47 StorageLaws.Read{U32.from_nat(ia(plan, cursor))})),
48 Fold.chosen(~O, ~g, operation, keep(plan, cursor), Fold.total(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, cursor),
49 Replayed.value(shape, fill, List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~ia, plan, cursor)), U32.from_nat(ia(plan, cursor)))),
50 Q):
51 +read = {StorageLaws.Read{U32.from_nat(ia(plan, cursor))} : StorageLaws.Op}
52 +seen = List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~ia, plan, cursor))
53 +before = Fold.total(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, cursor)
54 +x = Replayed.value(shape, fill, seen, U32.from_nat(ia(plan, cursor)))
55 +original = Replayed.value(shape, fill, ops, U32.from_nat(ia(plan, cursor)))
56 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, history => Replayed.storage(shape, fill, history),
57 List.append(&2, StorageLaws.Op, ops, Replayed.snoc(Pointwise.reads(~P, ~ia, plan, cursor), read)), Replayed.snoc(seen, read),
58 PointwiseProof.append_snoc(ops, Pointwise.reads(~P, ~ia, plan, cursor), read)) :
59 Shaped(~O, ~g, ~P, ~ia, ~keep, rest, operation, plan, shape, 1n+cursor, _, Fold.chosen(~O, ~g, operation, keep(plan, cursor), before, x), Q)
60 %Equal.cong(F32, F32, w => Fold.chosen(~O, ~g, operation, keep(plan, cursor), before, w), original, x,
61 Equal.sym(F32, x, original, PointwiseProof.value_reads(~P, ~ia, plan, cursor, shape, fill, ops, U32.from_nat(ia(plan, cursor))))) :
62 Shaped(~O, ~g, ~P, ~ia, ~keep, rest, operation, plan, shape, 1n+cursor, PointwiseProof.input_storage(~P, ~ia, plan, shape, fill, ops, 1n+cursor), _, Q)
63 next
64
65def step_lift(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
66 +rest: Nat, +operation: O, +plan: P, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +cursor: Nat,
67 inside: {Nat.is_lt(U32.to_nat(U32.from_nat(ia(plan, cursor))), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
68 -Q: Core.Dynamic & Result<&2, &1, Core.Error, F32> -> Type,
69 next: Start(~O, ~g, ~P, ~ia, ~keep, rest, operation, plan, shape, fill, ops, 1n+cursor, Q)) ->
70 Start(~O, ~g, ~P, ~ia, ~keep, 1n+rest, operation, plan, shape, fill, ops, cursor, Q):
71 +seen = List.append(&2, StorageLaws.Op, ops, Pointwise.reads(~P, ~ia, plan, cursor))
72 +before = Fold.total(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, cursor)
73 fits =>
74 Replayed.read_lift(shape, fill, seen, fits, U32.from_nat(ia(plan, cursor)), inside,
75 pair => Q(Fold.step(~O, ~g, operation, keep(plan, cursor),
76 input => value => Fold.loop(~O, ~g, ~P, ~ia, ~keep, rest, operation, plan, 1n+cursor, input, value),
77 before, Core.read_dynamic_result(shape, pair))),
78 after => shift(~O, ~g, ~P, ~ia, ~keep, rest, operation, plan, shape, fill, ops, cursor, Q, next)(after))
79
80def loop_lift(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
81 +fuel: Nat, +operation: O, +plan: P, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +cursor: Nat, +count: Nat,
82 +steps: {Nat.add(cursor, fuel) == count : Nat},
83 +inside: {Pointwise.inside(~P, ~ia, plan, count, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
84 -Q: Core.Dynamic & Result<&2, &1, Core.Error, F32> -> Type,
85 h: Final(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, count, Q)) ->
86 Start(~O, ~g, ~P, ~ia, ~keep, fuel, operation, plan, shape, fill, ops, cursor, Q):
87 match fuel:
88 case 0n:
89 final_at(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, count, cursor,
90 Equal.sym(Nat, cursor, count, PointwiseProof.steps_done(cursor, count, steps)), Q, h)
91 case 1n+rest:
92 +below = PointwiseProof.cursor_below(cursor, rest, count, steps)
93 step_lift(~O, ~g, ~P, ~ia, ~keep, rest, operation, plan, shape, fill, ops, cursor,
94 PointwiseProof.word_inside(ia(plan, cursor), shape,
95 PointwiseProof.inside_at(~P, ~ia, plan, count, Shape.logical_numel(Shape.dimensions(shape)), inside, cursor, below)),
96 Q, loop_lift(~O, ~g, ~P, ~ia, ~keep, rest, operation, plan, shape, fill, ops, 1n+cursor, count,
97 PointwiseProof.steps_next(cursor, rest, count, steps), inside, Q, h))
98
99def start_cast(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
100 +fuel: Nat, +operation: O, +plan: P, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>,
101 -Q: Core.Dynamic & Result<&2, &1, Core.Error, F32> -> Type,
102 start: Start(~O, ~g, ~P, ~ia, ~keep, fuel, operation, plan, shape, fill, ops, 0n, Q)) ->
103 Shaped(~O, ~g, ~P, ~ia, ~keep, fuel, operation, plan, shape, 0n, Replayed.storage(shape, fill, ops), 0.0, Q):
104 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, history => Replayed.storage(shape, fill, history),
105 List.append(&2, StorageLaws.Op, ops, Nil{}), ops, PointwiseProof.append_nil(ops)) :
106 Shaped(~O, ~g, ~P, ~ia, ~keep, fuel, operation, plan, shape, 0n, _, 0.0, Q)
107 start
108
109def run_lift(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
110 +operation: O, +plan: P, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat,
111 +inside: {Pointwise.inside(~P, ~ia, plan, count, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
112 -Q: Core.Dynamic & Result<&2, &1, Core.Error, F32> -> Type,
113 h: Final(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, count, Q)) ->
114 Shaped(~O, ~g, ~P, ~ia, ~keep, count, operation, plan, shape, 0n, Replayed.storage(shape, fill, ops), 0.0, Q):
115 start_cast(~O, ~g, ~P, ~ia, ~keep, count, operation, plan, shape, fill, ops, Q,
116 loop_lift(~O, ~g, ~P, ~ia, ~keep, count, operation, plan, shape, fill, ops, 0n, count, {==}, inside, Q, h))
117
118def contract(~O: Data, ~g: O -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~keep: P -> Nat -> Bool,
119 +operation: O, +plan: P, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +count: Nat,
120 +inside: {Pointwise.inside(~P, ~ia, plan, count, Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
121 -fits: {Lifecycle.logical_length(Replayed.storage(shape, fill, ops)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
122 Records.FoldContract<shape, Fold.total(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, count),
123 other => Replayed.value(shape, fill, ops, other),
124 Fold.run(~O, ~g, ~P, ~ia, ~keep, operation, plan, count, Core.Packed{shape, Core.TTensor{Replayed.storage(shape, fill, ops), fits}})>:
125 Records.FoldContract{
126 run_lift(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, count, inside,
127 result => {Fold.value(result) == Some{Fold.total(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, count)} : Maybe<&2, F32>},
128 after => {==})(fits),
129 other => within =>
130 run_lift(~O, ~g, ~P, ~ia, ~keep, operation, plan, shape, fill, ops, count, inside,
131 result => {Fold.input_point(result, other) == Some{Replayed.value(shape, fill, ops, other)} : Maybe<&2, F32>},
132 after => PointwiseProof.input_point(~P, ~ia, plan, count, shape, fill, ops, after, other, within))(fits)}
133
134def PairShaped(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
135 +fuel: Nat, +operation: O, +plan: P, +left: Shape.Shape, +right: Shape.Shape, +cursor: Nat,
136 -left_storage: Storage.Storage, -right_storage: Storage.Storage, +accumulator: F32,
137 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type) -> Type:
138 @-left_fits: {Lifecycle.logical_length(left_storage) == Shape.logical_numel(Shape.dimensions(left)) : Nat} ->
139 @-right_fits: {Lifecycle.logical_length(right_storage) == Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
140 Q(Fold.pair_loop(~O, ~g, ~P, ~ia, ~ib, fuel, operation, plan, cursor,
141 Core.Packed{left, Core.TTensor{left_storage, left_fits}}, Core.Packed{right, Core.TTensor{right_storage, right_fits}}, accumulator))
142
143def PairStart(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
144 +fuel: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
145 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +cursor: Nat,
146 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type) -> Type:
147 PairShaped(~O, ~g, ~P, ~ia, ~ib, fuel, operation, plan, left, right, cursor,
148 PointwiseProof.input_storage(~P, ~ia, plan, left, left_fill, left_ops, cursor),
149 PointwiseProof.input_storage(~P, ~ib, plan, right, right_fill, right_ops, cursor),
150 Fold.pair_total(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor), Q)
151
152def PairFinal(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
153 +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
154 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat,
155 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type) -> Type:
156 @-left_fits: {Lifecycle.logical_length(PointwiseProof.input_storage(~P, ~ia, plan, left, left_fill, left_ops, count)) ==
157 Shape.logical_numel(Shape.dimensions(left)) : Nat} ->
158 @-right_fits: {Lifecycle.logical_length(PointwiseProof.input_storage(~P, ~ib, plan, right, right_fill, right_ops, count)) ==
159 Shape.logical_numel(Shape.dimensions(right)) : Nat} ->
160 Q(((Core.Packed{left, Core.TTensor{PointwiseProof.input_storage(~P, ~ia, plan, left, left_fill, left_ops, count), left_fits}},
161 Core.Packed{right, Core.TTensor{PointwiseProof.input_storage(~P, ~ib, plan, right, right_fill, right_ops, count), right_fits}}),
162 Done{Fold.pair_total(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count)}))
163
164def pair_final_at(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
165 +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
166 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, -end: Nat, -count: Nat,
167 same: {end == count : Nat}, -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type,
168 h: PairFinal(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, end, Q)) ->
169 PairFinal(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, Q):
170 %same : PairFinal(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, _, Q)
171 h
172
173def pair_shift(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
174 +rest: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
175 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +cursor: Nat,
176 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type,
177 next: PairStart(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+cursor, Q)) ->
178 PairShaped(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, right, 1n+cursor,
179 Replayed.storage(left, left_fill, Replayed.snoc(List.append(&2, StorageLaws.Op, left_ops, Pointwise.reads(~P, ~ia, plan, cursor)),
180 StorageLaws.Read{U32.from_nat(ia(plan, cursor))})),
181 Replayed.storage(right, right_fill, Replayed.snoc(List.append(&2, StorageLaws.Op, right_ops, Pointwise.reads(~P, ~ib, plan, cursor)),
182 StorageLaws.Read{U32.from_nat(ib(plan, cursor))})),
183 g(operation, Fold.pair_total(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor),
184 Replayed.value(left, left_fill, List.append(&2, StorageLaws.Op, left_ops, Pointwise.reads(~P, ~ia, plan, cursor)), U32.from_nat(ia(plan, cursor))),
185 Replayed.value(right, right_fill, List.append(&2, StorageLaws.Op, right_ops, Pointwise.reads(~P, ~ib, plan, cursor)), U32.from_nat(ib(plan, cursor)))),
186 Q):
187 +left_read = {StorageLaws.Read{U32.from_nat(ia(plan, cursor))} : StorageLaws.Op}
188 +right_read = {StorageLaws.Read{U32.from_nat(ib(plan, cursor))} : StorageLaws.Op}
189 +left_seen = List.append(&2, StorageLaws.Op, left_ops, Pointwise.reads(~P, ~ia, plan, cursor))
190 +right_seen = List.append(&2, StorageLaws.Op, right_ops, Pointwise.reads(~P, ~ib, plan, cursor))
191 +before = Fold.pair_total(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor)
192 +x = Replayed.value(left, left_fill, left_seen, U32.from_nat(ia(plan, cursor)))
193 +y = Replayed.value(right, right_fill, right_seen, U32.from_nat(ib(plan, cursor)))
194 +left_word = Replayed.value(left, left_fill, left_ops, U32.from_nat(ia(plan, cursor)))
195 +right_word = Replayed.value(right, right_fill, right_ops, U32.from_nat(ib(plan, cursor)))
196 -right_after = Replayed.storage(right, right_fill, Replayed.snoc(right_seen, right_read))
197 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, history => Replayed.storage(left, left_fill, history),
198 List.append(&2, StorageLaws.Op, left_ops, Replayed.snoc(Pointwise.reads(~P, ~ia, plan, cursor), left_read)), Replayed.snoc(left_seen, left_read),
199 PointwiseProof.append_snoc(left_ops, Pointwise.reads(~P, ~ia, plan, cursor), left_read)) :
200 PairShaped(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, right, 1n+cursor, _, right_after, g(operation, before, x, y), Q)
201 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, history => Replayed.storage(right, right_fill, history),
202 List.append(&2, StorageLaws.Op, right_ops, Replayed.snoc(Pointwise.reads(~P, ~ib, plan, cursor), right_read)), Replayed.snoc(right_seen, right_read),
203 PointwiseProof.append_snoc(right_ops, Pointwise.reads(~P, ~ib, plan, cursor), right_read)) :
204 PairShaped(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, right, 1n+cursor,
205 PointwiseProof.input_storage(~P, ~ia, plan, left, left_fill, left_ops, 1n+cursor), _, g(operation, before, x, y), Q)
206 %Equal.trans(F32, g(operation, before, left_word, right_word), g(operation, before, x, right_word), g(operation, before, x, y),
207 Equal.cong(F32, F32, w => g(operation, before, w, right_word), left_word, x,
208 Equal.sym(F32, x, left_word, PointwiseProof.value_reads(~P, ~ia, plan, cursor, left, left_fill, left_ops, U32.from_nat(ia(plan, cursor))))),
209 Equal.cong(F32, F32, w => g(operation, before, x, w), right_word, y,
210 Equal.sym(F32, y, right_word, PointwiseProof.value_reads(~P, ~ib, plan, cursor, right, right_fill, right_ops, U32.from_nat(ib(plan, cursor)))))) :
211 PairShaped(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, right, 1n+cursor,
212 PointwiseProof.input_storage(~P, ~ia, plan, left, left_fill, left_ops, 1n+cursor),
213 PointwiseProof.input_storage(~P, ~ib, plan, right, right_fill, right_ops, 1n+cursor), _, Q)
214 next
215
216def pair_step_lift(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
217 +rest: 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>, +cursor: Nat,
219 left_inside: {Nat.is_lt(U32.to_nat(U32.from_nat(ia(plan, cursor))), Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool},
220 right_inside: {Nat.is_lt(U32.to_nat(U32.from_nat(ib(plan, cursor))), Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool},
221 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type,
222 next: PairStart(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+cursor, Q)) ->
223 PairStart(~O, ~g, ~P, ~ia, ~ib, 1n+rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor, Q):
224 +left_seen = List.append(&2, StorageLaws.Op, left_ops, Pointwise.reads(~P, ~ia, plan, cursor))
225 +right_seen = List.append(&2, StorageLaws.Op, right_ops, Pointwise.reads(~P, ~ib, plan, cursor))
226 +left_index = U32.from_nat(ia(plan, cursor))
227 +right_index = U32.from_nat(ib(plan, cursor))
228 +before = Fold.pair_total(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor)
229 +x = Replayed.value(left, left_fill, left_seen, left_index)
230 left_fits => right_fits =>
231 Replayed.read_lift(left, left_fill, left_seen, left_fits, left_index, left_inside,
232 pair => Q(Fold.pair_left(~O, ~g, operation, right_index,
233 left => right => value => Fold.pair_loop(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, 1n+cursor, left, right, value),
234 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_seen), right_fits}}, before,
235 Core.read_dynamic_result(left, pair))),
236 left_after => Replayed.read_lift(right, right_fill, right_seen, right_fits, right_index, right_inside,
237 pair => Q(Fold.pair_right(~O, ~g, operation,
238 left => right => value => Fold.pair_loop(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, 1n+cursor, left, right, value),
239 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, Replayed.snoc(left_seen, StorageLaws.Read{left_index})), left_after}},
240 before, x, Core.read_dynamic_result(right, pair))),
241 right_after => pair_shift(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor,
242 Q, next)(left_after, right_after)))
243
244def pair_loop_lift(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
245 +fuel: Nat, +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
246 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +cursor: Nat, +count: Nat,
247 +steps: {Nat.add(cursor, fuel) == count : Nat},
248 +left_inside: {Pointwise.inside(~P, ~ia, plan, count, Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool},
249 +right_inside: {Pointwise.inside(~P, ~ib, plan, count, Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool},
250 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type,
251 h: PairFinal(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, Q)) ->
252 PairStart(~O, ~g, ~P, ~ia, ~ib, fuel, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor, Q):
253 match fuel:
254 case 0n:
255 pair_final_at(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, cursor,
256 Equal.sym(Nat, cursor, count, PointwiseProof.steps_done(cursor, count, steps)), Q, h)
257 case 1n+rest:
258 +below = PointwiseProof.cursor_below(cursor, rest, count, steps)
259 pair_step_lift(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, cursor,
260 PointwiseProof.word_inside(ia(plan, cursor), left,
261 PointwiseProof.inside_at(~P, ~ia, plan, count, Shape.logical_numel(Shape.dimensions(left)), left_inside, cursor, below)),
262 PointwiseProof.word_inside(ib(plan, cursor), right,
263 PointwiseProof.inside_at(~P, ~ib, plan, count, Shape.logical_numel(Shape.dimensions(right)), right_inside, cursor, below)),
264 Q, pair_loop_lift(~O, ~g, ~P, ~ia, ~ib, rest, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+cursor, count,
265 PointwiseProof.steps_next(cursor, rest, count, steps), left_inside, right_inside, Q, h))
266
267def pair_start_cast(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
268 +fuel: Nat, +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>,
270 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type,
271 start: PairStart(~O, ~g, ~P, ~ia, ~ib, fuel, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, Q)) ->
272 PairShaped(~O, ~g, ~P, ~ia, ~ib, fuel, operation, plan, left, right, 0n,
273 Replayed.storage(left, left_fill, left_ops), Replayed.storage(right, right_fill, right_ops), 0.0, Q):
274 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, history => Replayed.storage(left, left_fill, history),
275 List.append(&2, StorageLaws.Op, left_ops, Nil{}), left_ops, PointwiseProof.append_nil(left_ops)) :
276 PairShaped(~O, ~g, ~P, ~ia, ~ib, fuel, operation, plan, left, right, 0n, _, Replayed.storage(right, right_fill, right_ops), 0.0, Q)
277 %Equal.cong(List<&2, StorageLaws.Op>, Storage.Storage, history => Replayed.storage(right, right_fill, history),
278 List.append(&2, StorageLaws.Op, right_ops, Nil{}), right_ops, PointwiseProof.append_nil(right_ops)) :
279 PairShaped(~O, ~g, ~P, ~ia, ~ib, fuel, operation, plan, left, right, 0n,
280 PointwiseProof.input_storage(~P, ~ia, plan, left, left_fill, left_ops, 0n), _, 0.0, Q)
281 start
282
283def pair_run_lift(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
284 +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
285 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat,
286 +left_inside: {Pointwise.inside(~P, ~ia, plan, count, Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool},
287 +right_inside: {Pointwise.inside(~P, ~ib, plan, count, Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool},
288 -Q: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, F32> -> Type,
289 h: PairFinal(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, Q)) ->
290 PairShaped(~O, ~g, ~P, ~ia, ~ib, count, operation, plan, left, right, 0n,
291 Replayed.storage(left, left_fill, left_ops), Replayed.storage(right, right_fill, right_ops), 0.0, Q):
292 pair_start_cast(~O, ~g, ~P, ~ia, ~ib, count, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, Q,
293 pair_loop_lift(~O, ~g, ~P, ~ia, ~ib, count, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 0n, count,
294 {==}, left_inside, right_inside, Q, h))
295
296def pair_contract(~O: Data, ~g: O -> F32 -> F32 -> F32 -> F32, ~P: Data, ~ia: P -> Nat -> Nat, ~ib: P -> Nat -> Nat,
297 +operation: O, +plan: P, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>,
298 +right: Shape.Shape, +right_fill: F32, +right_ops: List<&2, StorageLaws.Op>, +count: Nat,
299 +left_inside: {Pointwise.inside(~P, ~ia, plan, count, Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool},
300 +right_inside: {Pointwise.inside(~P, ~ib, plan, count, Shape.logical_numel(Shape.dimensions(right))) == True{} : Bool},
301 -left_fits: {Lifecycle.logical_length(Replayed.storage(left, left_fill, left_ops)) == Shape.logical_numel(Shape.dimensions(left)) : Nat},
302 -right_fits: {Lifecycle.logical_length(Replayed.storage(right, right_fill, right_ops)) == Shape.logical_numel(Shape.dimensions(right)) : Nat}) ->
303 Records.PairFoldContract<left, right,
304 Fold.pair_total(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count),
305 other => Replayed.value(left, left_fill, left_ops, other), other => Replayed.value(right, right_fill, right_ops, other),
306 Fold.pair_run(~O, ~g, ~P, ~ia, ~ib, operation, plan, count,
307 Core.Packed{left, Core.TTensor{Replayed.storage(left, left_fill, left_ops), left_fits}},
308 Core.Packed{right, Core.TTensor{Replayed.storage(right, right_fill, right_ops), right_fits}})>:
309 Records.PairFoldContract{
310 pair_run_lift(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, left_inside, right_inside,
311 result => {Fold.pair_value(result) ==
312 Some{Fold.pair_total(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count)} : Maybe<&2, F32>},
313 left_after => right_after => {==})(left_fits, right_fits),
314 other => within =>
315 pair_run_lift(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, left_inside, right_inside,
316 result => {Fold.left_point(result, other) == Some{Replayed.value(left, left_fill, left_ops, other)} : Maybe<&2, F32>},
317 left_after => right_after => PointwiseProof.input_point(~P, ~ia, plan, count, left, left_fill, left_ops, left_after, other, within))(left_fits, right_fits),
318 other => within =>
319 pair_run_lift(~O, ~g, ~P, ~ia, ~ib, operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, count, left_inside, right_inside,
320 result => {Fold.right_point(result, other) == Some{Replayed.value(right, right_fill, right_ops, other)} : Maybe<&2, F32>},
321 left_after => right_after => PointwiseProof.input_point(~P, ~ib, plan, count, right, right_fill, right_ops, right_after, other, within))(left_fits, right_fits)}