def indices_found

bendtorch-core@0.1.0.0 · src/autograd/reduce_to_fold_PROOF.bend:121

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Projection
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/broadcast_proof.bend as BroadcastProof
import bendtorch-core@0.1.0.0/src/autograd/reduce_fold_PROOF.bend as FoldProof

121def indices_found(+plan: Shape.BroadcastPlan, +cursor: Nat,
122  +below: {Nat.is_lt(cursor, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}) ->
123  {Projection.indices_result(Elementwise.input_indices(plan, U32.from_nat(cursor))) ==
124    Some{(target_index(plan, cursor), source_index(plan, cursor))} : Maybe<&1, U32 & U32>}:
125  Equal.trans(Maybe<&1, U32 & U32>, Projection.indices_result(Elementwise.input_indices(plan, U32.from_nat(cursor))),
126    Projection.offset_spec(plan, U32.to_nat(U32.from_nat(cursor))), Some{(target_index(plan, cursor), source_index(plan, cursor))},
127    Projection.input_indices_refines(plan, U32.from_nat(cursor)),
128    %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, PointwiseProof.word_exact(cursor, Shape.output_shape(plan), below)) :
129      {Projection.offset_spec(plan, _) == Some{(target_index(plan, cursor), source_index(plan, cursor))} : Maybe<&1, U32 & U32>}
130    FoldProof.offsets_walk(plan, Shape.index_map(plan), cursor, BroadcastProof.output_inside(plan, cursor, below)))