ElementwiseParallelProof.output_cell: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as ElementwiseParallelProof Lines 469-500 of bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&start_line=469&end_line=500 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/storage/model.bend as Model import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality # At an index below the output's element count, the parallel build holds the # value `expected` names there. def output_cell(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +depth: Nat, +length: Nat, +valid: {Storage.bounds(depth, length) == True{} : Bool}, +exact: {length == Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))) : Nat}, -left: Core.Dynamic, -right: Core.Dynamic, la: Array, ra: Array, +dl: Nat, +dr: Nat, -left_valid: Model.Balanced(F32, dl, la), -right_valid: Model.Balanced(F32, dr, ra), -left_reads: SourceReads(left, dl, la), -right_reads: SourceReads(right, dr, ra), +left_fits: {Totality.dimensions(left) == Shape.dimensions(Shape.left_shape(plan)) : List<&2, U32>}, +right_fits: {Totality.dimensions(right) == Shape.dimensions(Shape.right_shape(plan)) : List<&2, U32>}, +index: U32, +bound: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))) -> Fact<{Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}>: +inside = output_inside(plan, length, index, exact, bound) +within = output_bound(plan, index, bound) +position = output_position(depth, length, index, valid, inside) Fact{Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)), want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)), Elementwise.expected(operation, plan, left, right, index), {\{Fact: q => q} : Fact<({Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)) : Maybe<&2, F32>})> -> {Model.observe(F32, depth, Elementwise.build(depth, Elementwise.splits(depth), operation, plan, length, 0n, la, ra), Refinement.route(depth, index)) == want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)) : Maybe<&2, F32>}}( build_cell(depth, Elementwise.splits(depth), operation, plan, length, 0n, dl, dr, la, ra, Refinement.route(depth, index), %Equal.sym(Nat, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), U32.to_nat(index), position) : {Nat.is_lt(_, length) == True{} : Bool} inside, left_valid, right_valid)), Equal.trans(Maybe<&2, F32>, want(operation, plan, dl, dr, la, ra, Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n)), want(operation, plan, dl, dr, la, ra, U32.to_nat(index)), Elementwise.expected(operation, plan, left, right, index), Equal.cong(Nat, Maybe<&2, F32>, at => want(operation, plan, dl, dr, la, ra, at), Nat.add(Model.offset(depth, Refinement.route(depth, index)), 0n), U32.to_nat(index), position), Equal.trans(Maybe<&2, F32>, want(operation, plan, dl, dr, la, ra, U32.to_nat(index)), Elementwise.expected_left(operation, right, U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))), Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index)))))), Elementwise.expected(operation, plan, left, right, index), pick_expected(operation, Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))))), right, U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))), Model.observe(F32, dr, ra, Refinement.route(dr, U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))))), right_reads(U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))))(side_inside(right, Shape.right_shape(plan), Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index)), right_fits, right_walk_bound(plan, Shape.index_map(plan), U32.to_nat(index), within)))), Equal.trans(Maybe<&2, F32>, Elementwise.expected_left(operation, right, U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))), Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index)))))), Elementwise.expected_left(operation, right, U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))), Core.checked_observe_dynamic(left, U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))))), Elementwise.expected(operation, plan, left, right, index), Equal.cong(Maybe<&2, F32>, Maybe<&2, F32>, value => Elementwise.expected_left(operation, right, U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))), value), Model.observe(F32, dl, la, Refinement.route(dl, U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))))), Core.checked_observe_dynamic(left, U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index)))), left_reads(U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))))(side_inside(left, Shape.left_shape(plan), Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index)), left_fits, left_walk_bound(plan, Shape.index_map(plan), U32.to_nat(index), within)))), Equal.sym(Maybe<&2, F32>, Elementwise.expected(operation, plan, left, right, index), Elementwise.expected_left(operation, right, U32.from_nat(Elementwise.right_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))), Core.checked_observe_dynamic(left, U32.from_nat(Elementwise.left_walk(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), U32.to_nat(index))))), decided_walks(operation, plan, left, right, U32.to_nat(index), Shape.bool_case(Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan)))), within))))))} Uses (52): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LT https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_map https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=left_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=right_shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe_dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=left_walk https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=right_walk https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=splits https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=SourceReads https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=build_cell https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=decided_walks https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=left_walk_bound https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=output_bound https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=output_inside https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=output_position https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=pick_expected https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=right_walk_bound https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=side_inside https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=want https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=dimensions