BinaryProofs.write_spec: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend as BinaryProofs Lines 111-154 of bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&start_line=111&end_line=154 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index import bendtorch-core@0.1.0.0/src/storage/model.bend as Model 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/elementwise.bend as Elementwise import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts # Writing cell k at the path whose position is k turns the spec for k into # the spec for 1 + k. def write_spec(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +left: Shape.Shape, +left_fill: F32, +left_ops: List<&2, StorageLaws.Op>, +right: Shape.Shape, +right_fill: F32, +right_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, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, depth, base), path, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k)) == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, depth, base) : Array}: match depth: case 0n: %h : {ALeaf{cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, _)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base, Nat.is_lt(base, 1n+_))} : Array} %Equal.sym(Bool, Nat.is_lt(base, 1n+base), True{}, Facts.lt_self_succ(base)) : {ALeaf{cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, base)} == ALeaf{out_leaf(operation, plan, left, left_fill, left_ops, right, right_fill, right_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, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base), rest, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k)), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), write_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base, rest, h)) : {ANode{_, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high)} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array} %Equal.sym(Array, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), above(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, inside)) : {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_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, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), below(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, base, lower)) : {ANode{_, ArrayCore.write_path(F32, inner, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), rest, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k))} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array} %Equal.sym(Array, ArrayCore.write_path(F32, inner, out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high), rest, cell(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k)), out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, high), write_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, k, inner, high, rest, shifted)) : {ANode{out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, inner, base), _} == out_spec(operation, plan, left, left_fill, left_ops, right, right_fill, right_ops, 1n+k, 1n+inner, base) : Array} {==} Uses (32): 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=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=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/binary_proofs.bend&name=above https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&name=below https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&name=cell https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&name=out_leaf https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs.bend&name=out_spec 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/elementwise.bend&name=Operation