def right_positive

bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_proofs.bend:360

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/tensor/contracts/broadcast.bend as Broadcast
import bendtorch-core@0.1.0.0/src/tensor/contracts/broadcast_proof.bend as BroadcastProof

360def right_positive(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
361  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>},
362  +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(Shape.output_shape(plan)))) == True{} : Bool}) -> {Nat.is_lt(0n, U32.to_nat(Shape.count(right))) == True{} : Bool}:
363  +walk = Broadcast.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), 0n)
364  positive_of_lt(walk, U32.to_nat(Shape.count(right)),
365    Equal.trans(Bool, Nat.is_lt(walk, U32.to_nat(Shape.count(right))), Nat.is_lt(walk, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))), True{},
366      Equal.cong(Nat, Bool, x => Nat.is_lt(walk, x), U32.to_nat(Shape.count(right)), Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan))), right_count(left, right, plan, planned)),
367      BroadcastProof.right_walk_bound(plan, Shape.index_map(plan), 0n, output_positive(plan, d, fits))))