def pair_shift

bendtorch-core@0.1.0.0 · src/tensor/contracts/fold_proof.bend:173

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof
import bendtorch-core@0.1.0.0/src/tensor/contracts/fold.bend as Fold

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