GatherLAWS.gather_build_cells: law of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as GatherLAWS Lines 237-272 of bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&start_line=237&end_line=272 import Base 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/tensor/gather.bend as Gather # For a balanced input array A, a balanced index array I and every split, # the slot of the forward build that holds output cell (o, k, r), below # the count, holds input cell (o, j, r), where j is the entry the cell # reads: the word PyTorch's index_select and gather put there. law gather_build_cells: for +depth: Nat for +splits: Nat for +kind: Gather.Lookup for +outer: Nat for +rows: Nat for +inner: Nat for +count: Nat for +cells: Nat for +base: Nat for +da: Nat for -A: Array for a: Array for same: {a == A : Array} for valid: Model.Balanced(F32, da, A) for +di: Nat for -I: Array for index: Array for same_index: {index == I : Array} for index_valid: Model.Balanced(U32, di, I) for +path: Model.Path(depth) for +o: Nat for +k: Nat for +r: Nat for k_below: {Nat.is_lt(k, count) == True{} : Bool} for r_below: {Nat.is_lt(r, inner) == True{} : Bool} for at: {Nat.add(Model.offset(depth, path), base) == position(count, inner, o, k, r) : Nat} for in_count: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), cells) == True{} : Bool} for +j: U32 for read: {Model.observe(U32, di, I, Refinement.route(di, U32.from_nat(entry_at(kind, count, inner, o, k, r)))) == Some{j} : Maybe<&2, U32>} Holds<{Model.observe(F32, depth, Gather.build(depth, splits, Gather.Plan{kind, outer, rows, inner, count}, cells, base, a, index), path) == Model.observe(F32, da, A, Refinement.route(da, U32.from_nat(position(rows, inner, o, U32.to_nat(j), r)))) : Maybe<&2, F32>}> 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.get 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.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=Sigma 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/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/storage/refinement.bend&name=route https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=second https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Lookup https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=cell https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=entry https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=looked https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=source https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=Holds https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=entry_at https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=position https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=build_cells https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=entry_read https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=looked_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=read_entry https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=source_at 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