PermuteBuildProof.write_spec: 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 623-666 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=623&end_line=666 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/contracts/build_facts.bend as Facts import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws import bendtorch-core@0.1.0.0/src/storage/api.bend as Api import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore # Writing cell k at the path whose position is k turns the spec for k into # the spec for 1 + k. def write_spec(+input: Shape.Shape, +axes: List<&2, U32>, +fill: F32, +ops: List<&2, StorageLaws.Op>, +k: Nat, +depth: Nat, +base: Nat, +path: Model.Path(depth), +h: {Nat.add(Model.offset(depth, path), base) == k : Nat}) -> {ArrayCore.write_path(F32, depth, spec(input, axes, fill, ops, k, depth, base), path, word(input, axes, fill, ops, k)) == spec(input, axes, fill, ops, 1n+k, depth, base) : Array}: match depth: case 0n: %h : {ALeaf{word(input, axes, fill, ops, _)} == ALeaf{leaf(input, axes, fill, ops, base, Nat.is_lt(base, 1n+_))} : Array} %Equal.sym(Bool, Nat.is_lt(base, 1n+base), True{}, Facts.lt_self_succ(base)) : {ALeaf{word(input, axes, fill, ops, base)} == ALeaf{leaf(input, axes, fill, ops, base, _)} : Array} {==} case 1n+inner: Model.Step{+bit, +rest} = path match bit: case False{}: +c = Model.capacity(inner) +high = Nat.add(c, base) +inside = Equal.trans(Bool, Nat.is_lt(k, high), Nat.is_lt(Nat.add(Model.offset(inner, rest), base), high), True{}, Equal.cong(Nat, Bool, x => Nat.is_lt(x, high), k, Nat.add(Model.offset(inner, rest), base), Equal.sym(Nat, Nat.add(Model.offset(inner, rest), base), k, h)), Facts.lt_add_right(Model.offset(inner, rest), c, base, Api.offset_lt(inner, rest))) %Equal.sym(Array, ArrayCore.write_path(F32, inner, spec(input, axes, fill, ops, k, inner, base), rest, word(input, axes, fill, ops, k)), spec(input, axes, fill, ops, 1n+k, inner, base), write_spec(input, axes, fill, ops, k, inner, base, rest, h)) : {ANode{_, spec(input, axes, fill, ops, k, inner, high)} == spec(input, axes, fill, ops, 1n+k, 1n+inner, base) : Array} %Equal.sym(Array, spec(input, axes, fill, ops, k, inner, high), spec(input, axes, fill, ops, 1n+k, inner, high), above(input, axes, fill, ops, k, inner, high, inside)) : {ANode{spec(input, axes, fill, ops, 1n+k, inner, base), _} == spec(input, axes, fill, ops, 1n+k, 1n+inner, base) : Array} {==} case True{}: +c = Model.capacity(inner) +high = Nat.add(c, base) +off = Model.offset(inner, rest) +lower = Equal.trans(Bool, Nat.is_le(high, k), Nat.is_le(high, Nat.add(c, Nat.add(off, base))), True{}, Equal.cong(Nat, Bool, x => Nat.is_le(high, x), k, Nat.add(c, Nat.add(off, base)), Equal.trans(Nat, k, Nat.add(Nat.add(c, off), base), Nat.add(c, Nat.add(off, base)), Equal.sym(Nat, Nat.add(Nat.add(c, off), base), k, h), Equal.sym(Nat, Nat.add(c, Nat.add(off, base)), Nat.add(Nat.add(c, off), base), Index.add_assoc(c, off, base)))), Facts.le_add_cong(c, base, Nat.add(off, base), Api.le_add_left(off, base))) +shifted = Equal.trans(Nat, Nat.add(off, high), Nat.add(Nat.add(c, off), base), k, Facts.position_step(c, off, base), h) %Equal.sym(Array, spec(input, axes, fill, ops, k, inner, base), spec(input, axes, fill, ops, 1n+k, inner, base), below(input, axes, fill, ops, k, inner, base, lower)) : {ANode{_, ArrayCore.write_path(F32, inner, spec(input, axes, fill, ops, k, inner, high), rest, word(input, axes, fill, ops, k))} == spec(input, axes, fill, ops, 1n+k, 1n+inner, base) : Array} %Equal.sym(Array, ArrayCore.write_path(F32, inner, spec(input, axes, fill, ops, k, inner, high), rest, word(input, axes, fill, ops, k)), spec(input, axes, fill, ops, 1n+k, inner, high), write_spec(input, axes, fill, ops, k, inner, high, rest, shifted)) : {ANode{spec(input, axes, fill, ops, 1n+k, inner, base), _} == spec(input, axes, fill, ops, 1n+k, 1n+inner, base) : Array} {==} Uses (31): 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=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_le 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=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/index_proofs.bend&name=add_assoc 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/api.bend&name=le_add_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=offset_lt https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&name=write_path 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=Step https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=capacity 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/contracts/build_facts.bend&name=le_add_cong https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=lt_add_right https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=lt_self_succ https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend&name=position_step https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=above https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=leaf https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=spec https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=word