1	import Base
2	import ../../shape/core.bend as Shape
3	import ../../storage/main.bend as Storage
4	import ../../storage/LAWS.bend as StorageLaws
5	import ../core.bend as Core
6	import ../lifecycle.bend as Lifecycle
7	import ./replayed.bend as Replayed
8	import ./pointwise.bend as Pointwise
9	import ./pointwise_proof.bend as PointwiseProof
10	import ./fold.bend as Fold
11	import ./fold_records.bend as Records
12	
13	def 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	
19	def 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	
25	def 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	
33	def 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	
41	def 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	
65	def 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	
80	def 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	
99	def 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	
109	def 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	
118	def 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	
134	def 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	
143	def 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	
152	def 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	
164	def 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	
173	def 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	
216	def 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	
244	def 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	
267	def 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	
283	def 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	
296	def 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)}