PermuteBuildProof.output_word: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteBuildProof Lines 396-431 of bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&start_line=396&end_line=431 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Values import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build import bendtorch-core@0.1.0.0/src/storage/model.bend as Model import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts # What the parallel build holds at output index `other`. def output_word(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan, +d: Nat, +n: Nat, +valid: {Storage.bounds(d, n) == True{} : Bool}, +exact: {n == Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))) : Nat}, +ds: Nat, -c: Array, -bc: Model.Balanced(F32, ds, c), +other: Nat, +earlier: {Nat.is_lt(other, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}) -> Fact<{Lifecycle.checked_observe_array(d, n, Build.build(d, Build.Request{input, axes}, n, c), U32.from_nat(other)) == Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>}>: +index = U32.from_nat(other) +inside = length_below(Layout.output(input, axes, plan), n, exact, other, earlier) +at = Equal.trans(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), U32.to_nat(index), other, Facts.output_position(d, n, index, valid, inside), word_below(Layout.output(input, axes, plan), other, earlier)) +below : {Nat.is_lt(other, n) == True{} : Bool} = %Equal.sym(Nat, n, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), exact) : {Nat.is_lt(other, _) == True{} : Bool} earlier -built = Build.build(d, Build.Request{input, axes}, n, c) -recipe = Build.recipe(Build.Request{input, axes}) Fact{Equal.trans(Maybe<&2, F32>, Lifecycle.checked_observe_array(d, n, built, index), Model.observe(F32, d, built, Refinement.route(d, index)), Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))}, owned_observe(d, n, built, index, valid, inside), Equal.trans(Maybe<&2, F32>, Model.observe(F32, d, built, Refinement.route(d, index)), Some{Pair.fst(F32, Array & Array, Build.cell(recipe, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), (c, Array.new(F32, 0n, 0.0)), Nat.is_lt(Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), n)))}, Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))}, {\{Fact: q => q} : Fact<{Model.observe(F32, d, built, Refinement.route(d, index)) == Some{Pair.fst(F32, Array & Array, Build.cell(recipe, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), (c, Array.new(F32, 0n, 0.0)), Nat.is_lt(Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), n)))} : Maybe<&2, F32>}> -> {Model.observe(F32, d, built, Refinement.route(d, index)) == Some{Pair.fst(F32, Array & Array, Build.cell(recipe, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), (c, Array.new(F32, 0n, 0.0)), Nat.is_lt(Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), n)))} : Maybe<&2, F32>}}( build_cell(d, input, axes, n, ds, c, Refinement.route(d, index), bc)), %Equal.sym(Nat, Nat.add(Model.offset(d, Refinement.route(d, index)), 0n), other, at) : {Some{Pair.fst(F32, Array & Array, Build.cell(recipe, _, (c, Array.new(F32, 0n, 0.0)), Nat.is_lt(_, n)))} == Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>} %Equal.sym(Bool, Nat.is_lt(other, n), True{}, below) : {Some{Pair.fst(F32, Array & Array, Build.cell(recipe, other, (c, Array.new(F32, 0n, 0.0)), _))} == Some{Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other))))} : Maybe<&2, F32>} Equal.cong(F32, Maybe<&2, F32>, word => Some{word}, Pair.fst(F32, Array & Array, Build.cell(recipe, other, (c, Array.new(F32, 0n, 0.0)), True{})), Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other)))), {\{Fact: q => q} : Fact<{Pair.fst(F32, Array & Array, Build.cell(recipe, other, (c, Array.new(F32, 0n, 0.0)), True{})) == Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other)))) : F32}> -> {Pair.fst(F32, Array & Array, Build.cell(recipe, other, (c, Array.new(F32, 0n, 0.0)), True{})) == Refinement.second(F32, Array.get(F32, c, U32.from_nat(Values.permute_source_index(input, axes, other)))) : F32}}( cell_word(input, axes, c, other)))))} Uses (43): 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=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.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=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/shape/core.bend&name=Shape 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=logical_numel 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/storage/refinement.bend&name=second https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=output_position https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=checked_observe_array https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/observation.bend&name=permute_source_index https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=Request https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=build https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=cell https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=recipe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=Fact https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=build_cell https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=cell_word https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=length_below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=owned_observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=word_below