def left_positive

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

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

350# An output with a cell reads a cell of each input, so neither input is empty.
351def left_positive(+left: Shape.Shape, +right: Shape.Shape, +plan: Shape.BroadcastPlan,
352  +planned: {Shape.broadcast_checked(left, right) == Done{plan} : Result<&2, &2, Shape.Error, Shape.BroadcastPlan>},
353  +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(left))) == True{} : Bool}:
354  +walk = Broadcast.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), 0n)
355  positive_of_lt(walk, U32.to_nat(Shape.count(left)),
356    Equal.trans(Bool, Nat.is_lt(walk, U32.to_nat(Shape.count(left))), Nat.is_lt(walk, Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan)))), True{},
357      Equal.cong(Nat, Bool, x => Nat.is_lt(walk, x), U32.to_nat(Shape.count(left)), Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan))), left_count(left, right, plan, planned)),
358      BroadcastProof.left_walk_bound(plan, Shape.index_map(plan), 0n, output_positive(plan, d, fits))))