ElementwiseParallelProof.build_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 205-242 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=205&end_line=242 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/tensor/elementwise.bend as Elementwise import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic # An inside cell of the parallel build holds what `want` names there: the # generic law of `Parallel.build`, with the elementwise cell. def build_cell(+depth: Nat, +splits: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +count: Nat, +base: Nat, +dl: Nat, +dr: Nat, -A: Array, -B: Array, +path: Model.Path(depth), -inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool}, -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) -> Fact<{Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path) == want(operation, plan, dl, dr, A, B, Nat.add(Model.offset(depth, path), base)) : Maybe<&2, F32>}>: +position = Nat.add(Model.offset(depth, path), base) -split = {\{Fact: q => q} : Fact<({Pair.fst(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array} & {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array})> -> {Pair.fst(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array} & {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}}( split_equal(dl, dr, A, B, left_valid, right_valid)) Fact{Equal.trans(Maybe<&2, F32>, Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path), Some{Pair.fst(F32, Array & Array, cell_of(operation, plan, position, A, B, True{}))}, want(operation, plan, dl, dr, A, B, position), %inside : {Model.observe(F32, depth, Elementwise.build(depth, splits, operation, plan, count, base, A, B), path) == Some{Pair.fst(F32, Array & Array, cell_of(operation, plan, position, A, B, _))} : Maybe<&2, F32>} {\{Generic.Fact: q => q} : Generic.Fact, ~Array, ~Elementwise.cell_at, Elementwise.walk(Elementwise.Request{operation, plan}), (A, B), depth, count, base, Elementwise.build(depth, splits, operation, plan, count, base, A, B))> -> Generic.Cells(~Elementwise.Walk, ~Array, ~Array, ~Elementwise.cell_at, Elementwise.walk(Elementwise.Request{operation, plan}), (A, B), depth, count, base, Elementwise.build(depth, splits, operation, plan, count, base, A, B))}( Generic.build_cells(~Elementwise.Request, ~Elementwise.Walk, ~Array, ~Array, ~Elementwise.walk, ~Elementwise.split, ~Elementwise.cell_at, Elementwise.Request{operation, plan}, (A, B), depth, splits, count, base, (A, B), {==}, at => inside => {\{Fact: q => q} : Fact<({Pair.snd(F32, Array & Array, cell_of(operation, plan, at, A, B, inside)) == (A, B) : Array & Array})> -> {Pair.snd(F32, Array & Array, cell_of(operation, plan, at, A, B, inside)) == (A, B) : Array & Array}}( cell_keeps(operation, plan, dl, dr, A, B, at, inside, left_valid, right_valid)), Pair.fst({Pair.fst(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}, {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}, split), Pair.snd({Pair.fst(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}, {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, B))) == (A, B) : Array & Array}, split)))(path), Pair.snd({Pair.snd(F32, Array & Array, cell_of(operation, plan, position, A, B, True{})) == (A, B) : Array & Array}, {Some{Pair.fst(F32, Array & Array, cell_of(operation, plan, position, A, B, True{}))} == want(operation, plan, dl, dr, A, B, position) : Maybe<&2, F32>}, {\{Fact: q => q} : Fact<(CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{})))> -> CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))}( cell_out(operation, plan, dl, dr, A, B, position, left_valid, right_valid))))} Uses (34): 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.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32 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=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma 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/storage/model.bend&name=Balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Path 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/tensor/elementwise.bend&name=Operation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Request https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Walk 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=cell_at https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=split https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=walk https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=CellOut 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=cell_keeps https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=cell_of https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=cell_out https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=split_equal 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/parallel_proofs.bend&name=Cells https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=build_cells