ReduceReplayedProof.output_eq: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend as ReduceReplayedProof Lines 985-1012 of bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&start_line=985&end_line=1012 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/storage/LAWS.bend as StorageLaws import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore import bendtorch-core@0.1.0.0/src/storage/api.bend as Api import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_storage_proof.bend as Owned import bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend as Par import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce # The writes of every cell, replayed on the owned storage `created` makes for # the target, give the owned storage the parallel build fills. def output_eq(+plan: Shape.BroadcastPlan, +rows: List<&2, Shape.Row>, +rows_exact: {rows == Shape.index_table(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))) : List<&2, Shape.Row>}, +shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +h: List<&2, Api.Effect>, +dc: Nat, +fc: F32, +source: Par.Source, +target: Shape.Shape, +facts: Facts, +d: Nat, +fits: {Storage.bounds(d, U32.to_nat(Shape.count(target))) == True{} : Bool}, -f: {Storage.bounds(d, U32.to_nat(Shape.count(target))) == True{} : Bool}) -> {StorageLaws.replay(writes(plan, Shape.Indexed{rows, rows_exact}, shape, fill, ops, U32.to_nat(Shape.count(target))), Storage.Owned{d, U32.to_nat(Shape.count(target)), Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}) == Storage.Owned{d, U32.to_nat(Shape.count(target)), Reduce.build(d, parallel_splits(plan, d, U32.to_nat(Shape.count(target))), rows, Shape.extents(Shape.output_shape(plan)), U32.to_nat(Shape.count(target)), 0n, Api.arr(h, dc, fc)), Reduce.build_balanced(d, parallel_splits(plan, d, U32.to_nat(Shape.count(target))), rows, Shape.extents(Shape.output_shape(plan)), U32.to_nat(Shape.count(target)), 0n, Api.arr(h, dc, fc)), f} : Storage.Storage}: +n = U32.to_nat(Shape.count(target)) +map : PlanMap(plan) = Shape.Indexed{rows, rows_exact} +splits = parallel_splits(plan, d, n) +extents = Shape.extents(Shape.output_shape(plan)) Equal.trans(Storage.Storage, StorageLaws.replay(writes(plan, map, shape, fill, ops, n), Storage.Owned{d, n, Array.new(F32, d, 0.0), ArrayCore.new_balanced(F32, d, 0.0), f}), Storage.Owned{d, n, out_spec(plan, map, shape, fill, ops, n, d, 0n), out_balanced(plan, map, shape, fill, ops, n, d, 0n), f}, Storage.Owned{d, n, Reduce.build(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc)), Reduce.build_balanced(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc)), f}, chain(plan, map, shape, fill, ops, d, n, f, fits, Shape.count(target), Conversion.le_reflexive(n), n, Conversion.le_reflexive(n)), Owned.owned_eq(d, n, out_spec(plan, map, shape, fill, ops, n, d, 0n), Reduce.build(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc)), Equal.sym(Array, Reduce.build(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc)), out_spec(plan, map, shape, fill, ops, n, d, 0n), build_eq(plan, rows, rows_exact, shape, fill, ops, h, dc, fc, n, source, facts, d, splits, 0n)), out_balanced(plan, map, shape, fill, ops, n, d, 0n), f)(Reduce.build_balanced(d, splits, rows, extents, n, 0n, Api.arr(h, dc, fc)))) Uses (39): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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=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/autograd/reduce.bend&name=build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=build_balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=Facts https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=PlanMap https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=build_eq https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=chain https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=out_balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=out_spec https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=parallel_splits https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=writes 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=Index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=count 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_table 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=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/LAWS.bend&name=Op https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=replay https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=Effect https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&name=new_balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage 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/tensor/contracts/binary_storage_proof.bend&name=owned_eq https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/matmul_parallel_proof.bend&name=Source https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=le_reflexive