def walk_left_value

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

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

132def walk_left_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_left(Shape.index_table(left, right, output), Shape.Fin.value(Shape.numel(output), index)) == Shape.row_major(left, Shape.project_left(left, right, output, alignment, Shape.unflatten(output, index))) : Nat}:
133  +value = Shape.Fin.value(Shape.numel(output), index)
134  +ds = Shape.digits(output, value)
135  +nl = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, left))
136  +nr = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, right))
137  +coordinate = Shape.unflatten(output, index)
138  +projected = Shape.project_left(left, right, output, alignment, coordinate)
139  +strides = strides_of(left)
140  +dropped = List.drop(&2, Nat, ds, nl)
141  %Equal.sym(Nat, Shape.walk_left(Shape.index_rows(Shape.pad(nl, left), Shape.pad(nr, right), output), value), dot(strides_of(Shape.pad(nl, left)), ds), walk_left_rows(Shape.pad(nl, left), Shape.pad(nr, right), output, value, right_padded(left, right, output, alignment))) : {_ == Shape.row_major(left, projected) : Nat}
142  %Equal.cong(List<&2, Nat>, Nat, steps => dot(steps, ds), zeros(nl, strides), strides_of(Shape.pad(nl, left)), Equal.sym(List<&2, Nat>, strides_of(Shape.pad(nl, left)), zeros(nl, strides), pad_strides(nl, left))) : {_ == Shape.row_major(left, projected) : Nat}
143  %Equal.sym(Nat, dot(zeros(nl, strides), ds), dot(strides, dropped), dot_zeros(nl, ds, strides)) : {_ == Shape.row_major(left, projected) : Nat}
144  %Equal.sym(Nat, dot(strides, dropped), Shape.offset(left, Shape.broadcast_indices(left, dropped)), dot_broadcast(left, dropped)) : {_ == Shape.row_major(left, projected) : Nat}
145  %Equal.cong(Nat, Nat, width => Shape.offset(left, Shape.broadcast_indices(left, List.drop(&2, Nat, ds, Nat.sub(width, List.length(&2, Nat, left))))), List.length(&2, Nat, ds), List.length(&2, Nat, output), digits_length(output, value)) : {_ == Shape.row_major(left, projected) : Nat}
146  %Equal.cong(List<&2, Nat>, Nat, values => Shape.offset(left, Shape.project_indices(left, values)), Shape.indices(output, coordinate), ds, Coordinates.digits_unflatten(output, index)) : {_ == Shape.row_major(left, projected) : Nat}
147  %Equal.cong(List<&2, Nat>, Nat, values => Shape.offset(left, values), Shape.indices(left, projected), Shape.project_indices(left, Shape.indices(output, coordinate)), Broadcast.project_left(left, right, output, alignment, coordinate)) : {_ == Shape.row_major(left, projected) : Nat}
148  Coordinates.offset_indices(left, projected)