def walk_right_value

bendtorch-core@0.1.0.0 · src/shape/projection_proofs.bend:150

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates

150def walk_right_value(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Broadcast<left, right, output>, +index: Shape.Fin(Shape.numel(output))) -> {Shape.walk_right(Shape.index_table(left, right, output), Shape.Fin.value(Shape.numel(output), index)) == Shape.row_major(right, Shape.project_right(left, right, output, alignment, Shape.unflatten(output, index))) : Nat}:
151  +value = Shape.Fin.value(Shape.numel(output), index)
152  +ds = Shape.digits(output, value)
153  +nl = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, left))
154  +nr = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, right))
155  +coordinate = Shape.unflatten(output, index)
156  +projected = Shape.project_right(left, right, output, alignment, coordinate)
157  +strides = strides_of(right)
158  +dropped = List.drop(&2, Nat, ds, nr)
159  %Equal.sym(Nat, Shape.walk_right(Shape.index_rows(Shape.pad(nl, left), Shape.pad(nr, right), output), value), dot(strides_of(Shape.pad(nr, right)), ds), walk_right_rows(Shape.pad(nl, left), Shape.pad(nr, right), output, value, left_padded(left, right, output, alignment))) : {_ == Shape.row_major(right, projected) : Nat}
160  %Equal.cong(List<&2, Nat>, Nat, steps => dot(steps, ds), zeros(nr, strides), strides_of(Shape.pad(nr, right)), Equal.sym(List<&2, Nat>, strides_of(Shape.pad(nr, right)), zeros(nr, strides), pad_strides(nr, right))) : {_ == Shape.row_major(right, projected) : Nat}
161  %Equal.sym(Nat, dot(zeros(nr, strides), ds), dot(strides, dropped), dot_zeros(nr, ds, strides)) : {_ == Shape.row_major(right, projected) : Nat}
162  %Equal.sym(Nat, dot(strides, dropped), Shape.offset(right, Shape.broadcast_indices(right, dropped)), dot_broadcast(right, dropped)) : {_ == Shape.row_major(right, projected) : Nat}
163  %Equal.cong(Nat, Nat, width => Shape.offset(right, Shape.broadcast_indices(right, List.drop(&2, Nat, ds, Nat.sub(width, List.length(&2, Nat, right))))), List.length(&2, Nat, ds), List.length(&2, Nat, output), digits_length(output, value)) : {_ == Shape.row_major(right, projected) : Nat}
164  %Equal.cong(List<&2, Nat>, Nat, values => Shape.offset(right, Shape.project_indices(right, values)), Shape.indices(output, coordinate), ds, Coordinates.digits_unflatten(output, index)) : {_ == Shape.row_major(right, projected) : Nat}
165  %Equal.cong(List<&2, Nat>, Nat, values => Shape.offset(right, values), Shape.indices(right, projected), Shape.project_indices(right, Shape.indices(output, coordinate)), Broadcast.project_right(left, right, output, alignment, coordinate)) : {_ == Shape.row_major(right, projected) : Nat}
166  Coordinates.offset_indices(right, projected)